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 (mail at allan-blanchard.fr)
  • Date: Fri, 17 Jan 2020 13:52:31 +0100 (CET)

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>