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:

José N. Oliveira, Luís S. Barbosa, José B. Barros, Alcino Cunha, Maria João Frade and Jorge Sousa Pinto
Formal Methods in Software Engineering [link]
In University of Minho, 2007-2012