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:

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