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 18.0 (Argon) and relies on the following other sofware packages.

Package Version
Why3 0.88.3
Alt-Ergo 2.2.0
CVC4 1.6
CVC3 2.4.1
Z3 4.8.3
E Prover 2.2
Coq 8.7.2

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