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 17 (Chlorine-20180502) and relies on the following other sofware packages.
| Package | Version |
|---|---|
| Why3 | 0.88.3 |
| Alt-Ergo | 2.2.0 |
| CVC4 | 1.5 |
| CVC3 | 2.4.1 |
| Z3 | 4.6.0 |
| E Prover | 2.0 |
| Coq | 8.7.2 |
For more details on verifying the examples see the file README.txt.