lifo-2014.md

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.