package caisar-ovo

  1. Overview
  2. Docs
OVO parser for CAISAR

Install

Dune Dependency

git.frama-c.com Readme Changelog Edit opam file Versions (2)

Authors

  1. L
    LAISER team, Software Safety and Security Laboratory, CEA-List

Maintainers

  1. L
    LAISER team, Software Safety and Security Laboratory, CEA-List

Sources

caisar-0.2.tbz
sha256=e56829b9e2564c1cd0ab01798cc2b3c9b8887be0180b1e260b6e93940bf5e069
sha512=fcd1b1bf4b32d4ece982acab59710c8f1fe33784f5e4a15bd85a14cd1b7db450f529a0bfca31009a919008312149a25c6ea7ec3272d524a1e4c026eeeff7d5a3

CHANGES.md.html

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.