# OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems

arXiv: https://arxiv.org/abs/2108.01220 · HTML: https://mlsanity.com/paper/2108.01220/

## Key facts

- Cited by 38 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 44 references that are in the map.
- First posted on arXiv 3 Aug 2021.

## Builds on (most cited first, 14 of 14)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [DeepDriving: Learning Affordance for Direct Perception in Autonomous Driving](https://mlsanity.com/paper/1505.00256/) (2015)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems](https://mlsanity.com/paper/2005.02979/) (2020)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers](https://mlsanity.com/paper/1802.06981/) (2018)
- [Specification-Guided Safety Verification for Feedforward Neural Networks](https://mlsanity.com/paper/1812.06161/) (2018)

## Built on by (most cited first, 30 of 38)

- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Distributionally Robust Statistical Verification with Imprecise Neural Networks](https://mlsanity.com/paper/2308.14815/) (2023)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [Bayesian Safety Validation for Failure Probability Estimation of Black-Box Systems](https://mlsanity.com/paper/2305.02449/) (2023)
- [Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops](https://mlsanity.com/paper/2410.00145/) (2024)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems](https://mlsanity.com/paper/2407.14394/) (2024)
- [Predictive Uncertainty for Runtime Assurance of a Real-Time Computer Vision-Based Landing System](https://mlsanity.com/paper/2508.09732/) (2025)
- [Fail-Safe Adversarial Generative Imitation Learning](https://mlsanity.com/paper/2203.01696/) (2022)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems](https://mlsanity.com/paper/2505.03643/) (2025)
- [Verifying Inverse Model Neural Networks](https://mlsanity.com/paper/2202.02429/) (2022)
- [ICODE: Modeling Dynamical Systems with Extrinsic Input Information](https://mlsanity.com/paper/2411.13914/) (2024)
- [NP-Hard Lower Bound Complexity for Semantic Self-Verification](https://mlsanity.com/paper/2501.15446/) (2025)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Interpretable Local Tree Surrogate Policies](https://mlsanity.com/paper/2109.08180/) (2021)

## Abstract (arXiv)

Deep learning methods can be used to produce control policies, but certifying their safety is challenging. The resulting networks are nonlinear and often very large. In response to this challenge, we present OVERT: a sound algorithm for safety verification of nonlinear discrete-time closed loop dynamical systems with neural network control policies. The novelty of OVERT lies in combining ideas from the classical formal methods literature with ideas from the newer neural network verification literature. The central concept of OVERT is to abstract nonlinear functions with a set of optimally tight piecewise linear bounds. Such piecewise linear bounds are designed for seamless integration into ReLU neural network verification tools. OVERT can be used to prove bounded-time safety properties by either computing reachable sets or solving feasibility queries directly. We demonstrate various examples of safety verification for several classical benchmark examples. OVERT compares favorably to existing methods both in computation time and in tightness of the reachable set.