alpha-beta-CROWN: An Efficient, Scalable and GPU Accelerated Neural Network Verifier (winner of VNN-COMP 2021, 2022, 2023, 2024, 2025)
Neural Network Verification Software Tool https://www.verivital.com Documentation:
Lyapunov-stable Neural Control for State and Output Feedback
DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
A lightweight Python package for setting up robustness experiments and to compute robustness distributions.
WraAct is a tool to construct the convex hull of various activation functions.
Abstract Constraint Transformation
Auto-Verify is a framework for neural network verification, that allows you to install, configure and Neural Network verifiers in parallel portfolios
WraLU is an artifact for the paper "ReLU Hull Approximation" (POPL'24), which provides a sound but incomplete neural network verifier by over-approximating ReLU function hull.
NCubeV - The Nonlinear Neural Network Verifier
Research MoE application in safety-critical system at Institute of Software Integrated System - Vanderbilt University
lattice theory playground
Uses the simplex to propose a tighter boundary for the l1 perturbation of the convex activation function network, improving the effect of the CROWN algorithm.
Adversarial attacks and certified defences on a small MNIST network — FGSM, αβ-CROWN, interval analysis, randomised smoothing.
SART: Sign-Absolute Reformulation Theory for Binary Variable Reduction in Neural Network Verification
Verification of Neural Network Control Systems in Continuous Time
WraAct is an artifact for the paper "Convex Hull Approximation for Activation Functions" (OOPSLA'25), which provides a sound but incomplete neural network verifiers by over-approximating the function hulls of various activation functions (including leaky ReLU, ReLU, sigmoid, tanh, and maxpool).
Verification of neural networks based on input splitting and forward propagation of symbolic intervals with fresh variables.
This repository contains a collection of fully connected benchmarks from VNNCOMP 2022-2024. It is designed to offer a more organized version of the existing benchmarks, making it easier to test new software. We recommend cloning the 'benchmarks_vnncomp' repository, which includes this repository as a submodule.
Add a description, image, and links to the neural-network-verification topic page so that developers can more easily learn about it.
To associate your repository with the neural-network-verification topic, visit your repo's landing page and select "manage topics."