# NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

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

## Key facts

- Cited by 128 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Apr 2020.

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

- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [PRoA: A Probabilistic Robustness Assessment against Functional Perturbations](https://mlsanity.com/paper/2207.02036/) (2022)
- [CertiFair: A Framework for Certified Global Fairness of Neural Networks](https://mlsanity.com/paper/2205.09927/) (2022)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [How Generalizable Is My Behavior Cloning Policy? A Statistical Approach to Trustworthy Performance Evaluation](https://mlsanity.com/paper/2405.05439/) (2024)
- [Shielding Atari Games with Bounded Prescience](https://mlsanity.com/paper/2101.08153/) (2021)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/2304.01218/) (2023)
- [Distributionally Robust Statistical Verification with Imprecise Neural Networks](https://mlsanity.com/paper/2308.14815/) (2023)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference](https://mlsanity.com/paper/2309.09187/) (2023)

## Abstract (arXiv)

This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks and the second deals with the safety verification of a deep learning-based adaptive cruise control system.