ACSL by Example
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.1 and relies among others on the following sofware packages.
| Package | Version |
|---|---|
| Why3 | 1.2.1 |
| Alt-Ergo | 2.3.0 |
| CVC4 | 1.6 |
| CVC3 | 2.4.1 |
| Z3 | 4.8.6 |
| 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,
see the the
file .travis
for details.
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.