Software

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.