Slides
The slides used during the lecture are available here.
Lab sessions
- exercises on formal systems and Floyd-Hoare system are available here
- lab session on the Jessie/Why/Alt-Ergo toolchain is available here. The archive containing skeletons is available here.
Project
The lecture is evaluated on a project that is here
Some references and useful websites
- L. Correnson and al. Frama-C User Manual — Release Fluorine-20130601. 2013 pdf
- P. Baudin and al. ACSL: ANSI/ISO C Specification Language — Version 1.7, Fluorine-20130601. 2013 pdf
- V. Prevosto. ACSL Tutorial. pdf
- J. Burghardt and al. ACSL by Example. A fairly complete tour of ACSL features through various functions inspired from C++ STL. 2014 pdf
- Frama-C publications link
