Tutoriel Wp Save

Frama-C and WP tutorial

Project README

About this 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 and after, 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.

It can be used for both learning and teaching, I hope you will have some fun with it :) .

The last version is available on my website in English and in French.

An online French version is available on Zeste de Savoir.


In order to build the files, you can use docker

docker build -t tutoriel_wp .
docker run --rm -v $PWD:/mnt -w /mnt tutoriel_wp make
Open Source Agenda is not affiliated with "Tutoriel Wp" Project. README Source: AllanBlanchard/tutoriel_wp
Open Issues
Last Commit
6 months ago

Open Source Agenda Badge

Open Source Agenda Rating