Examples & Tutorials¶

Worked examples demonstrating NNV’s verification capabilities across 10+ application domains, from image classification to power systems.

Recommended Learning Path¶

Start here: Quick Start – your first verification
Image classification: Image Classification – MNIST, GTSRB robustness
Safety-critical systems: ACAS Xu Collision Avoidance – ACAS Xu with ONNX/VNNLIB
Control systems: Control Systems – ACC, AEBS closed-loop verification
Advanced topics: GNNs, Neural ODEs, probabilistic verification

You can run any example directly:

cd('code/nnv/examples');
run('Tutorial/NN/MNIST/verify.m')             % Image classification
run('Tutorial/NN/ACAS Xu/verify_onnx_vnnlib.m') % ACAS Xu with VNNLIB
run('Tutorial/NNCS/ACC/Verification/verify.m')  % Closed-loop control

Repository Folder Structure¶

examples/QuickStart/ – installation verification and first steps
examples/Tutorial/ – beginner-friendly walkthroughs (NN, NNCS, SPIE)
examples/NN/ – advanced neural network examples (CNN, RNN, GNN, NeuralODE, BNN)
examples/NNCS/ – advanced control system examples
examples/Submission/ – paper and competition reproduction code (ARCH-COMP, VNN-COMP, CAV, etc.)

Image Classification

MNIST, GTSRB, MedMNIST, CIFAR-10 – adversarial robustness verification for image classifiers.

Image Classification

ACAS Xu

Aviation collision avoidance – verifying all 45 ACAS Xu networks with ONNX and VNNLIB.

ACAS Xu Collision Avoidance

Semantic Segmentation

Pixel-level verification for M2NIST and CamVid segmentation networks.

Semantic Segmentation

Graph Neural Networks

GCN and GINE on IEEE bus systems for power grid safety verification.

Graph Neural Networks

Neural ODEs

Reachability of continuous-time dynamics: spiral, CartPole, FPA systems.

Recurrent Neural Networks

Sequence-based robustness verification with variable time horizons.

Recurrent Neural Networks

Control Systems

ACC, AEBS, Inverted Pendulum, DC-DC Buck converter – closed-loop safety verification.

Control Systems

Malware Detection

Adversarial robustness of DNN-based malware classifiers (BODMAS dataset).

Malware Detection

Medical Imaging

SPIE 2025 tutorial: 2D/3D classification and segmentation robustness for medical images.

Medical Imaging

Weight Perturbation

ModelStar verification under quantization, hardware faults, and model compression.

Weight Perturbation (ModelStar)

Fairness Verification

FairNNV counterfactual and individual fairness on financial benchmark datasets.

Fairness Verification (FairNNV)

Conference Tutorials

SPIE 2025, DSN 2024, EMSOFT 2023 – tutorial materials and references.

Conference Tutorials