Newer
Older
---
layout: clean_page
---
## Deductive Verification with Frama-C/WP
Context: course on Deductive Verification in [master
FIIL](https://www.universite-paris-saclay.fr/en/education/master/m2-fondements-de-linformatique-et-ingenierie-du-logiciel-foundations-of-computer#presentation-m2)
(2d year) at [University
Paris-Saclay](https://www.universite-paris-saclay.fr/en) (France), since
2015.
Teachers: [Andrei Paskevich](http://tertium.org/) (Why3) and [Julien
Signoles](http://julien.signoles.free.fr/index.en.html) (Frama-C).
Our exercises use both Frama-C/WP and [Why3](http://why3.lri.fr/) ([in a
browser](http://why3.lri.fr/try/)). [A
tarball](/assets/dokuwiki/wp-ups.tar.gz) 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.