package caisar-ovo

  1. Overview
  2. Docs
OVO parser for CAISAR


Dune Dependency





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.