A tutorial on the [WP plugin](http://www.frama-c.com/wp.html) has been
given at
[iFM 2013](http://www.it.abo.fi/iFM2013/workshops_and_tutorials.php) in
Turku (Finland), on June 11th, 2013.
[Slides](/assets/dokuwiki/tutorial/ifm-2013/slides.pdf) and [C
examples](/assets/dokuwiki/tutorial/ifm-2013/frama_c_tutorial_examples.tar.gz)
are available.

The examples archive contains both unannotated implementation as
exercises and a solution that can be entirely verified by the WP plug-in
as distributed in the Fluorine 2 (20130501) version of Frama-C. For the
more advanced examples, some special options of wp are needed in order
for the provers to complete the proof automatically. Theses options are
given at the bottom of each file.