A tutorial on the [E-ACSL plugin](http://www.frama-c.com/eacsl.html) has
been given at [RV 2013](http://rv2013.gforge.inria.fr/) in Rennes
(France), on September 24th, 2013.
[Slides](/assets/dokuwiki/tutorial/slides.pdf) and [C
examples](/assets/dokuwiki/tutorial/eacsl_examples.tgz) are available.

The examples archive contains both unannotated implementation as
exercises and a solution that can be entirely run by the E-ACSL plug-in
version 0.3 (with Frama-C Fluorine 20130601). The exact way to run each
example is given at the bottom of the corresponding file.