--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2019 ---
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>