On the occasion of the 114th birthday of french résistante Lucie Aubrac’s birth, we are happy to release CAISAR version 6.0.
The release source is available at our public forge and on opam.
We brought back Docker support, now using our own image registry instead of
Dockerhub.
CAISAR docker can come in two flavours: bare or solvers. The first image
provides the CAISAR binary, to test for interoperability within your
infrastructure. The second brings several supported provers with CAISAR,
allowing to use it right away. You can reproduce our examples, or write a specification of your own and launch a verification query!
To try CAISAR within Docker, type the following command:
docker pull registry.frama-c.com/pub/caisar:bare
See our official manual for detailed instructions.
CAISAR can now launch multiple provers on a given verification query. This
feature enables to compare solvers on the same task more easily. Each prover
launch can be configured with a specific precision and configuration set,
enabling fine-grained tuning of prover performances. We deprecate options
--prover-altern and --prover-precision as a result.
CAISAR base specification language, WhyML, allow to express complex properties like global robustness. CAISAR can compile down WhyML queries into the VNNLIB format; this format is the de facto standard for the international competition of Verification of Neural Network (VNN-COMP). By supporting VNNLIB, CAISAR can more easily interface with the VNN-COMP to reproduce benchmarks on all its supported provers.
Deprecate option --dataset as dataset filenames can be simply
defined via --define option.