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 16 (20171101 Sulfur) and relies on the following other sofware packages.
For more details on verifying the examples see the file README.txt.