Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C WP and ACSL tutorial for beginners

  • Subject: [Frama-c-discuss] Frama-C WP and ACSL tutorial for beginners
  • From: mail at allan-blanchard.fr (Allan Blanchard)
  • Date: Thu, 14 Dec 2017 14:31:35 +0100
Dear Frama-C users,

I have released the first english version of a tutorial about Frama-C 
with WP and ACSL. It is a tutorial for beginners that introduces the use 
of these tools but also provides some basic ideas about the theory 
behind the tools.

The PDF document is available through :

     http://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf

The markdown sources are available through my Github :

     https://github.com/AllanBlanchard/tutoriel_wp

This tutorial is the english translation (and I thank Jens Gerlach for 
his help during the translation) of the french tutorial I previously 
wrote, that is also available on the same Github repository but also on 
my website :

     http://allan-blanchard.fr/publis/frama-c-wp-tutoriel-fr.pdf

Any feedback is welcome. Do not hesitate to create issues or pull 
requests on my Github (in this last case, please modify the markdown 
files, the latex files are partially auto-generated from them). If you 
want some feature of ACSL or WP to be included in the tutorial, please 
let me know, I will do my best to add them.

I hope this document helps learning and teaching the use of Frama-C and WP.

Regards,

Allan Blanchard