Skip to content
Snippets Groups Projects
Select Git revision
  • feature/bdesloges/update-ivette-page
  • master default protected
  • improve-index-wip-proposal
  • fix/martin/fix-changelog-event-display
4 results
Blame Permalink
ifm-2013.md 748 B

A tutorial on the WP plugin has been given at iFM 2013 in Turku (Finland), on June 11th, 2013. Slides and C examples 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.