Teaching
Andrei Paskevich and Julien Signoles Course on Deductive Verification In University Paris Saclay, 2015 In French.
Course on Deductive Verification in Master MPRI (1st year) at University Paris-Saclay (France), given by Andrei Paskevich (Why3) and Julien Signoles (Frama-C), since 2015.
Our exercises use both Frama-C/WP and Why3 (in a browser). A tarball contains most of our material related to Frama-C/WP (in French, still evolving each year). The training exercises are embedded in slides, the ones for the final practical session are directly provided in .c files.
Martin Peres and Steve D. Lazaro Language-based security [link] In University College London, 2014
Guillaume Petiot, Alain Giorgetti, Jacques Julliand Course on Frama-C [link] In Université de Franche-Comté, 2013-2014 In French.
Eugene Kornykhin Formal Specification and Verification [link] In Moscow State University, 2012-2013 In Russian.
Virgile Prevosto, Julien Signoles and Tristan Le Gall Static Analysis Course In ENSIIE Evry, 2010-2018 In French.
Below is the list of exercices done with Frama-C during the Static Analysis Course at ENSIIE: