ACSL by Example

Replay Status

This repository contains ACSL by Example — a collection of C functions and data types whose behavior has been formally specified with ACSL and formally verified with Frama-C/WP.

The directory StandardAlgorithms contains the complete C source code including ACSL annotations of the examples.

This version of ACSL by Example is intended for Frama-C 19.0 and relies among others on the following sofware packages.

Package Version
Why3 1.2.0
Alt-Ergo 2.0.0
CVC4 1.6
CVC3 2.4.1
Z3 4.8.4
E Prover 2.3
Coq 8.9.1

For more details on verifying the examples see the file README.txt.

Travis CI

We have added Travis CI to demonstrate what steps are required to set up the toolchain. Travis performs the tests and replays the proofs with reduced timeouts. That means the results in Travis are possibly downgraded comparing to that we state in the tutorial and the Results folder. Verification results are also could be different on your machine either because of the hardware. Please look at StandardAlgorithms/README.txt for additional settings.