NNV

Matlab Toolbox for Neural Network Verification

This toolbox implements reachability methods for analyzing neural networks and control systems with neural network controllers in the area of autonomous cyber-physical systems (CPS).

Related tools and software

This toolbox makes use of the neural network model transformation tool (nnmt) and for closed-loop systems analysis, the hybrid systems model transformation and translation tool (HyST), and the COntinuous Reachability Analyzer (CORA).

Execution without installation:

NNV can be executed online without installing Matlab or other dependencies through CodeOcean via the following CodeOcean capsules:

Latest

CAV 2023 Tool Paper: https://doi.org/10.24433/CO.0803700.v1

Previous

CAV 2020 ImageStar paper version: https://doi.org/10.24433/CO.3351375.v1
CAV 2020 Tool paper version: https://doi.org/10.24433/CO.0221760.v1
Earliest version: https://doi.org/10.24433/CO.1314285.v1

Installation:

Clone or download the NNV toolbox from (https://github.com/verivital/nnv)

Note: to operate correctly, nnv depends on other tools (CORA, NNMT, HyST, onnx2nnv), which are included as git submodules. As such, you must clone recursively, e.g., with the following:
```
git clone --recursive https://github.com/verivital/nnv.git
```
If running in Ubuntu, install MATLAB and proceed to run the provided installation script (then, skip to step 6).
```
chmod +x install_ubuntu.sh
./install_ubuntu.sh
```
For MacOS and Windows, please install MATLAB (2023a or newer) with at least the following toolboxes:
- Computer Vision
- Control Systems
- Deep Learning
- Image Processing
- Optimization
- Parallel Computing
- Statistics and Machine Learning
- Symbolic Math
- System Identification

Install the following support package Deep Learning Toolbox Converter for ONNX Model Format

Note: Support packages can be installed in MATLAB's HOME tab > Add-Ons > Get Add-ons, search for the support package using the Add-on Explorer and click on the Install button.

Open MATLAB, then go to the directory where NNV exists on your machine, then run the install.m script located at /nnv/

Note: if you restart Matlab, rerun either install.m or startup_nnv.m, which will add the necessary dependencies to the path; you alternatively can run savepath after installation to avoid this step after restarting Matlab, but this may require administrative privileges
Optional installation packages

a. To run verification for convolutional neural networks (CNNs) on VGG16/VGG19, additional support packages must be installed:
- VGG16
- VGG19
b) To run MATLAB's neural network verification comparison, an additional support package is needed (used in CAV'2023 submission):
- Deep Learning Toolbox Verification Library
c) To load models from other deep learning frameworks, please install the additional support packages:
- TensorFlow and Keras: Deep Learning Toolbox Converter for TensorFlow Models
- PyTorch: Deep Learning Toolbox Converter for PyTorch Models
d) To use Conformal Prediction (CP) verification, set up a Python virtual environment:
```
# From the NNV root directory:
python -m venv .venv
# Windows: .venv\Scripts\activate
# macOS/Linux: source .venv/bin/activate
pip install -r requirement.txt
```
See PYTHON_SETUP.md for detailed instructions.

Uninstallation:

Open MATLAB, then go to the /code/nnv/ folder and execute the uninstall.m script.

What's New in NNV 3.0

NNV 3.0 introduces major new verification capabilities:

VolumeStar: Verification of video and 3D volumetric data (medical images)
FairNNV: Formal verification of neural network fairness
Probabilistic Verification: Scalable conformal prediction-based analysis
Weight Perturbation Analysis: Verification under quantization/hardware errors
Time-Dependent Networks: Variable-length time series verification
Malware Detection: New cybersecurity verification domain

See README_NNV3_CONTRIBUTIONS.md for full details on NNV 3.0 features.

Documentation

| Document | Description | |----------|-------------| | README_NNV3_CONTRIBUTIONS.md | NNV 3.0 new features and contributions | | README_TEST.md | Testing documentation and coverage | | code/nnv/examples/README.md | Examples navigation guide | | code/nnv/examples/QuickStart/ | Getting started examples | | code/nnv/examples/Tutorial/ | Step-by-step tutorials |

Getting started with NNV

Quick Start

New to NNV? Start with the QuickStart examples for installation verification and your first neural network verification.

cd examples/QuickStart
test_installation      % Verify your setup
simple_verification    % Your first verification

Troubleshooting? Run the diagnostic tool:

check_nnv_setup()

Tutorial

To get started with NNV, let's take a look at a tutorial containing examples demonstrating:

Robustness verification on the MNIST dataset.
- Includes model training and several verification examples.
Robustness verification on the GTSRB dataset.
- Includes model training and robustness verification.
Comparisons of exact (sound and complete) and approximate (sound and incomplete) methods using Star sets
- Visualize the size difference on the output sets and the computation times for each method.
Robustness analysis of a malware classifier (BODMAS Dataset).

NNCS

Reachability analysis of an inverted pendulum.
Safety verification example of an Adaptive Cruise Control (ACC) system.
Safety verification of an Automated Emergency Braking System

And more! Please go to the tutorial description for more details!

Examples

In addition to the examples from the tutorial, there are more examples in the 'code/nnv/examples/' folder, including:

Semantic Segmentation

Robustness analysis of semantic segmentation NNs

Recurrent Neural Networks

Robustness analysis of RNNs

Neural Ordinary Differential Equations

Reachability analysis of neural ODEs

And more other NN and NNCS examples.

Tests

To run all the tests, one can run the following command from 'code/nnv/tests/' folder:

runtests(pwd, 'IncludeSubfolders', true);

Paper Publications and Competitions

All the code for the publication using NNV, including competitions that NNV has participated in (e.g. VNNCOMP and ARCH-COMP) can be found in the examples/Submissions folder. For a selected subset of publications, tags were created. To reproduce those results, please download NNV using the corresponding tag or use the corresponding CodeOcean capsules.

Contributors

References

The methods implemented in NNV are based upon or used in the following papers:

Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, Taylor T. Johnson, "NNV 2.0: The Neural Network Verification Tool". In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13965. Springer, Cham. [https://doi.org/10.1007/978-3-031-37703-7_19]
Anne M Tumlin, Diego Manzanas Lopez, Preston Robinette, Yuying Zhao, Tyler Derr, and Taylor T Johnson. "FairNNV: The Neural Network Verification Tool For Certifying Fairness. In Proceedings of the 5th ACM International Conference on AI in Finance (ICAIF '24)". Association for Computing Machinery, New York, NY, USA, 36–44. [https://doi.org/10.1145/3677052.3698677]
Navid Hashemi, Samuel Sasaki, Ipek Oguz, Meiyi Ma, Taylor T. Johnson, "Scaling Data-Driven Probabilistic Robustness Analysis for Semantic Segmentation Neural Networks", 38th Conference on Neural Information Processing Systems (NeurIPS), 2025.
Samuel Sasaki, Diego Manzanas Lopez, Preston K. Robinette, Taylor T. Johnson, "Robustness Verification of Video Classification Neural Networks", IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), 2025

Nnv

Install / Use

README

NNV