Newer
Older
This page gather material that has been presented at the seminar of the
[LIFO laboratory](http://www.univ-orleans.fr/lifo/?lang=en) of Orléans
University on 2014-10-13.
- [slides from the
presentation](/mantis/frama-c/tutorial/lifo-2014/slides.pdf)
- [annotated
programs](/mantis/frama-c/tutorial/lifo-2014/solutions.tar.gz)
corresponding to the code shown in the slides. Note that the lemmas
in `binary_search_tree.c` cannot be discharged in the current
version of Frama-C, because WP does not generate a complete
environment.