Software

IVAN

Incremental and Complete Verification of Deep Neural Networks. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms.

FANC

Incremental and Incomplete Verification of Deep Neural Networks. This tool provides a technique for faster certification of Neural Networks (NNs) using proof transfer. Various approximations such as quantization, pruning, perforation, sampling, etc; are now widely used to speed up network inference. Post-training approximations change the weights of networks, and hence the original proof of certification of the network becomes invalid. Similarly, fine-tuning a neural network for repairing or other reasons, networks need to be verified again. Certification of network robustness is a computationally expensive task. Hence, in this work, we try to accelerate the certification proof of approximate or fine-tuned networks by transferring some information during the certification proof of the original network.

DeepJ

DeepJ is an interval-domain based analyzer that soundly over-approximates the Clarke Jacobian of a Lipschitz, but not necessarily differentiable function.

ELINA

State-of-the-art library for numerical program analysis. ELINA contains optimized implementations of popular numerical abstract domains such as Polyhedra, Octagon, Zonotope, DeepPoly, and Zones for static analysis. ELINA uses improved algorithms, online decomposition as well as state of the art performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement etc. to significantly improve the performance of static analysis with the numerical domains.

ERAN

State-of-the-art neural network verifier. ERAN produces state-of-the-art precision and performance for both complete and incomplete verification and can be tuned to provide best precision and scalability. The goal of ERAN is to automatically verify safety properties of neural networks with feedforward, convolutional, and residual layers against input perturbations (e.g., L∞-norm attacks, geometric transformations, vector field deformations, etc). ERAN supports fully-connected, convolutional, and residual networks with ReLU, Sigmoid, Tanh, and Maxpool activations and is sound under floating point arithmetic. It employs custom abstract domains which are specifically designed for the setting of neural networks and which aim to balance scalability and precision. Recently, ERAN verified the highest number of benchmarks at VNN-COMP'20.