# DNNV: A Framework for Deep Neural Network Verification

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

## Key facts

- Cited by 23 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 41 references that are in the map.
- First posted on arXiv 26 May 2021.

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

- [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)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [End-to-end Driving via Conditional Imitation Learning](https://mlsanity.com/paper/1710.02410/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Examples: Attacks and Defenses for Deep Learning](https://mlsanity.com/paper/1712.07107/) (2017)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [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)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [A Unified View of Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1711.00455/) (2017)
- [SOCRATES: Towards a Unified Platform for Neural Network Analysis](https://mlsanity.com/paper/2007.11206/) (2020)

## Built on by (most cited first, 23 of 23)

- [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)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Fairify: Fairness Verification of Neural Networks](https://mlsanity.com/paper/2212.06140/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Harnessing Neuron Stability to Improve DNN Verification](https://mlsanity.com/paper/2401.14412/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Online Safety Analysis for LLMs: a Benchmark, an Assessment, and a Path Forward](https://mlsanity.com/paper/2404.08517/) (2024)
- [Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers](https://mlsanity.com/paper/2202.05207/) (2022)
- [SoundnessBench: A Soundness Benchmark for Neural Network Verifiers](https://mlsanity.com/paper/2412.03154/) (2024)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Compiling High-Level Neural Network Specifications into VNN-LIB Queries](https://mlsanity.com/paper/2402.01353/) (2024)
- [Towards Developing Safety Assurance Cases for Learning-Enabled Medical Cyber-Physical Systems](https://mlsanity.com/paper/2211.15413/) (2022)
- [Expediting Neural Network Verification via Network Reduction](https://mlsanity.com/paper/2308.03330/) (2023)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [PCV: A Point Cloud-Based Network Verifier](https://mlsanity.com/paper/2301.11806/) (2023)
- [Reinfier and Reintrainer: Verification and Interpretation-Driven Safe Deep Reinforcement Learning Frameworks](https://mlsanity.com/paper/2410.15127/) (2024)
- [Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report](https://mlsanity.com/paper/2411.14163/) (2024)
- [Data-Driven Falsification of Cyber-Physical Systems](https://mlsanity.com/paper/2505.03863/) (2025)
- [Formal Reasoning About Confidence and Automated Verification of Neural Networks](https://mlsanity.com/paper/2511.07293/) (2025)

## Abstract (arXiv)

Despite the large number of sophisticated deep neural network (DNN) verification algorithms, DNN verifier developers, users, and researchers still face several challenges. First, verifier developers must contend with the rapidly changing DNN field to support new DNN operations and property types. Second, verifier users have the burden of selecting a verifier input format to specify their problem. Due to the many input formats, this decision can greatly restrict the verifiers that a user may run. Finally, researchers face difficulties in re-using benchmarks to evaluate and compare verifiers, due to the large number of input formats required to run different verifiers. Existing benchmarks are rarely in formats supported by verifiers other than the one for which the benchmark was introduced. In this work we present DNNV, a framework for reducing the burden on DNN verifier researchers, developers, and users. DNNV standardizes input and output formats, includes a simple yet expressive DSL for specifying DNN properties, and provides powerful simplification and reduction operations to facilitate the application, development, and comparison of DNN verifiers. We show how DNNV increases the support of verifiers for existing benchmarks from 30% to 74%.