Neural Network Verification Software

This page lists our software packages for the verification of systems using neural networks.

NSVerify

Neural System Verify is a software package for performing reachability analysis on neural agent-environment systems implemented by ReLU feed-forward neural networks. Further information can be found in the corresponding paper (published at KR 2018).

Click here to download the source code: NSVerify

RNSVerify

Recurrent Neural System Verify is an extension of NSVerify to handle recurrent neural networks. Further information can be found in the corresponding paper (published at AAAI 2019).

Click here to download the source code: RNSVerify

VeriNet

VeriNet is a symbolic interval propagation based verification algorithm for feed-forward neural networks. Further information can be found in the paper (To appear at ECAI20).

Click here to download the source code: VeriNet

VENUS

VErification of NeUral Systems is a state-of-the-art sound and complete verification toolkit for ReLU-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties. VENUS implements a MILP-based verification method whereby it leverages dependency relations between the ReLU nodes to prune the search tree that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting. Further information can be found in the corresponding paper (published at AAAI 2020).

Click here to download the source code: VENUS

NANESVerify

Neural Agent operating on a Non-deterministic Environment System Verify is a software package for performing MILP-based verification for agent-environment systems where the agent is controlled by ReLU-activated feed-forward neural networks, the environment is non-deterministic with branching temporal evolutions, and specifications are expressed in a bounded variant of CTL.

Click here to download the source code: NANESVerify