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] Tutorial: Introduction to C program proof with Frama-C and its WP plugin

  • Subject: [Frama-c-discuss] Tutorial: Introduction to C program proof with Frama-C and its WP plugin
  • From: mail at allan-blanchard.fr (Allan Blanchard)
  • Date: Wed, 29 May 2019 10:10:39 +0200
  • In-reply-to: <b94d4aec-9066-4eab-5092-205ac5d9a8da@allan-blanchard.fr>
  • References: <b94d4aec-9066-4eab-5092-205ac5d9a8da@allan-blanchard.fr>
Dear Frama-C users,

I have released a new version of "Introduction to C program proof with 
Frama-C and its WP plugin".

This tutorial targets beginners but also more advanced users. For 
beginners, we expect it to be a good introduction to the tools and the 
theory on which the tools rely. For more advanced users, a new chapter 
addressing some methodological aspects about proof with WP has been added.

All the examples have been tested on Frama-C 19 'Potassium' beta, thus 
the document is still tagged as beta version until the Frama-C 19 
'Potassium' is officially released.

The PDF document is available through:

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

The source code of the tutorial, examples, exercises and some coq proofs 
are available through GitHub:

https://github.com/AllanBlanchard/tutoriel_wp

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.

For french users who use to work with the french version of the 
tutorial, note that this new version is currently not available in 
french, I will work on it as soon as possible. It will be available in 
PDF but also online on the website "Zeste de Savoir".

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

Regards,

Allan Blanchard


PS: Summary of the changes since the previous version:

  * fixes all forgotten translations
  * adds about 70 exercises
  * gives some more details about \at
  * in formal aspects adds explanations about assignment with aliasing
    and functions calls
  * provides more details about the verification of loops
  * adds a small section about predicate overloading
  * adds a new example for lemmas
  * adds a section about inductive predicates
  * adds a new example for axiomatic definitions
  * adds explanations about contracts in ghost code
  * adds a chapter about methodology
      o minimal contracts for absence of runtime errors,
      o understand the proof context and use assertions to trigger lemmas
      o increase proof automation using lemma functions
  * a lot of minor improvements everywhere
  * ready for Frama-C Potassium

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190529/429e2ee2/attachment-0001.html>