--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2020 ---
[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




Dear Frama-C users, 




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

The PDF document is available through: 
[ https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf | 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 | https://github.com/AllanBlanchard/tutoriel_wp ] 


This version is a minor update mainly related to the new version of Frama-C (Calcium), but it also includes some minor fixes in some explanations and exercices. 





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. 

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




[ This part of the message is intentionnaly written in French ] 



Pour les utilisateurs français de ce tutoriel, sachez que la version française, à jour par rapport à la version anglaise, est de nouveau disponible à l'adresse : 
[ https://allan-blanchard.fr/publis/frama-c-wp-tutoriel-fr.pdf | https://allan-blanchard.fr/publis/frama-c-wp-tutoriel-fr.pdf ] 

La version sous forme de tutoriel en ligne sur la plateforme de partage de connaissances Zeste de Savoir est encore en travaux mais devrait suivre. 

[ end ] 

Regards, 
Allan Blanchard 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200117/74d7781a/attachment.html>