Frama-C+WP Tutorial

Frama-C (FRAmework for Modular Analysis of C programs) is a set of interoperable program analyzers for C programs. I have used this software during all my PhD thesis, mostly for deductive proof using the WP plugin. So, I wrote a tutorial that allows to learn ACSL (the specification language of Frama-C) and the use of WP by practice, also getting some theorical rudiments about deductive proof.

• PDF Version - EN
• PDF Version - FR

Of course, any feedback is welcome. Do not hesitate to create issues or pull requests on GitHub. If you want some features of ACSL or WP to be included in the tutorial, please let me know, I will do my best to add them.

• GitHub of the tutorial

Previous versions:

• PDF Version - EN - 20 Calcium
• PDF Version - FR - 20 Calcium
• Online Version - FR