package caisar-ovo

0.2 (19-06-2023)

• [prover] Integration of the nnenum prover.

• [prover] Integration of the $\alpha-\beta-$CROWN prover.

• [prover] Integration of the AIMOS metamorphic testing prover.

• [prover] Add printer for VNN-LIB format for property specification as supported by nnenum and $\alpha-\beta-$CROWN provers.

• [prover] Support for multiple configurations of provers, using the prover-altern command line option. An example of registering an alternate configuration is available under config/caisar-detection.conf

• [prover] Add transformation to translate ONNX format into SMTLIB format for allowing SMTLIB2 compliant provers to work on neural networks.

• [doc] The first version of the CAISAR manual is publicly available on our website. It includes detailed installation instructions, examples on the ACAS-Xu and MNIST local robustness benchmarks. Those examples use an experimental interpretation language that is not fully documented yet.

• [deps] Upgraded Why3 to 1.6.0 version.

• Add verify-json command for verifying a robustness property via a JSON configuration file.

• Add verification of datasets for classification tasks in terms of a specific CSV format: each line provides the label in 1st column, and data features in the other columns.

• Add support for memory and time limits.

• Add debug logging options.

0.1 (13-07-2022)

• First public release of CAISAR.