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