NNV Software Tool
NNV: Neural Network Verification Toolbox for MATLAB
NNV is an open-source MATLAB toolbox for the formal verification of deep neural networks and learning-enabled cyber-physical systems, developed by the VeriVITAL research group at Vanderbilt University. The crux of NNV is set-based reachability analysis using star sets and their extensions — Star, ImageStar, VolumeStar, and GraphStar — with both exact (sound and complete) and over-approximate (sound) reachability algorithms.
NNV verifies safety and robustness properties of feedforward, convolutional, recurrent, graph, and semantic segmentation networks, as well as neural ordinary differential equations and neural network control systems. It supports the community’s standard input formats, including ONNX networks and VNNLIB verification properties. The tool was first presented at CAV 2020 (Tran et al.), with NNV 2.0 following at CAV 2023 (Lopez et al.).
The latest release, NNV 3.0, has been accepted at ATVA and introduces verification of video and 3D volumetric data (VolumeStar), formal verification of graph neural networks (GNNV), verification under weight perturbations (ModelStar), formal fairness certification (FairNNV), and scalable probabilistic verification based on conformal prediction. The repository includes a six-experiment artifact-evaluation package (FairNNV, ProbVer, GNNV, VideoStar, ModelStar, and a tool comparison) reproducing the paper’s results. I am a contributor to NNV 3.0; the toolbox is led and maintained by the VeriVITAL group.