Skip to content
Snippets Groups Projects
Commit 6bf5a30e authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

[release] Updated changelog for release 0.2

parent fd473e70
No related branches found
No related tags found
No related merge requests found
## 0.1.1 (Unreleased) # 0.2 (19-06-2023)
- Add first version of the CAISAR manual. - [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
- Add `verify-json` command for verifying a robustness property via a JSON - Add `verify-json` command for verifying a robustness property via a JSON
configuration file. configuration file.
- Integration of the [nnenum](https://github.com/stanleybak/nnenum) prover.
- Add printer for VNN-LIB format for property specification as supported by the
`nnenum` prover.
- Add transformation to translate ONNX format into SMT-LIB format for allowing
classic solvers to understand and operate on neural networks.
- Add verification of datasets for classification tasks in terms of a specific - 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 CSV format: each line provides the label in 1st column, and data features in
the other columns. Also, add builtin implementations of min-max scaling and the other columns.
z-score normalization for data normalization. - Add builtin implementations of min-max scaling and z-score normalization for data normalization.
- Rework the section in `README.md` for obtaining CAISAR in order to mention the - Add support for memory limitation and timeout.
`opam` package just released. - Add debug logging options.
## 0.1 (13-07-2022) # 0.1 (13-07-2022)
First public release of CAISAR. First public release of CAISAR.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment