Teaching
Andrei Paskevich, Julien Signoles Course on Deductive Verification 2015 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.
Guillaume Petiot, Alain Giorgetti, Jacques Julliand Course on Frama-C [link] 2013-2014 Université de Franche-Comté, 2013-2014 In French.
Eugene Kornykhin Formal Specification and Verification [link] 2012-2013 Moscow State University, 2012-2013 In Russian.
Virgile Prevosto, Julien Signoles, Tristan Le Gall Static Analysis Course 2010-2018 ENSIIE Evry, 2010-2018 In French.
Below is the list of exercices done with Frama-C during the Static Analysis Course at ENSIIE: