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: Thu, 2 Jul 2020 08:26:29 +0200 (CEST)

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 ] 


The previous (Calcium) version is still available through: 


[ https://allan-blanchard.fr/frama-c-wp-tutorial.html | https://allan-blanchard.fr/frama-c-wp-tutorial.html ] 




This version is mainly an update to follow the changes in Scandium 21.1 release, that includes new ACSL and WP features, but also contains new exercises and a few fixes. 





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. 




Detailed changes: 

    * Contracts 
        * Adds WP smoke tests 
        * More exercises for behaviors 
            * Merged exercises 1 to 4 into a single one 
            * Adds two simple exercises 
        * Two new exercises for WP modularity 
    * ACSL properties 
        * Removes a paragraph that was too dependent of provers versions 
        * Slightly changes two exercises so that the proof is harder for SMT solvers 
    * ACSL logic definitions 
        * Updates the section about ghosts with Frama-C 21 new features 
            * ghost typing (and ghost qualifier) 
            * CFG checking 
        * Adds exercises about these new features 
        * The verification that inductive definitions are well founded is now done through Why3 
    * VI 
        * Updates ghost elements to be compliant with Frama-C 21 

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



Pour les utilisateurs français de ce tutoriel, la version PDF est elle aussi mise à jour : 
[ https://allan-blanchard.fr/publis/frama-c-wp-tutoriel-fr.pdf | https://allan-blanchard.fr/publis/frama-c-wp-tutoriel-fr.pdf ] 

La version disponible en ligne sur Zeste deSavoir est toujours la version Calcium : 
[ https://zestedesavoir.com/tutoriels/885/introduction-a-la-preuve-de-programmes-c-avec-frama-c-et-son-greffon-wp/ | https://zestedesavoir.com/tutoriels/885/introduction-a-la-preuve-de-programmes-c-avec-frama-c-et-son-greffon-wp/ ] 
La version Scandium devrait suivre relativement rapidement, elle est déjà disponible en bêta, mais cela nécessite un compte (gratuit) sur la plateforme Zeste de Savoir : 
[ https://zestedesavoir.com/contenus/beta/885/introduction-a-la-preuve-de-programmes-c-avec-frama-c-et-son-greffon-wp/ | https://zestedesavoir.com/contenus/beta/885/introduction-a-la-preuve-de-programmes-c-avec-frama-c-et-son-greffon-wp/ ] 

Quand la version publiquement disponible sera mise à jour vers Scandium, l'ancienne version ne sera plus disponible sur Zeste de Savoir. 

[ end ] 

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