diff --git a/CHANGES.md b/CHANGES.md index 00c35278fb0dd45b97c087e3ed5ed2853ba95779..03525f62fca4491151c92b65c7c2d315a6c4e912 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,28 +1,42 @@ # 0.2 (19-06-2023) -- [prover] Integration of the [nnenum](https://github.com/stanleybak/nnenum) prover. -- [prover] Integration of the [$\alpha-\beta-$CROWN](https://github.com/stanleybak/nnenum) prover. +- [prover] Integration of the [nnenum](https://github.com/stanleybak/nnenum) + prover. + +- [prover] Integration of the + [$\alpha-\beta-$CROWN](https://github.com/stanleybak/nnenum) 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 available - publicly on our [website](caisar-platform.com/documentation). - 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 + +- [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](caisar-platform.com/documentation). 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 builtin implementations of min-max scaling and z-score normalization for data normalization. -- Add support for memory limitation and timeout. + +- Add support for memory and time limits. + - Add debug logging options. # 0.1 (13-07-2022) -First public release of CAISAR. +- First public release of CAISAR.