Vincent Penelle

Ressources à consulter :

La documentation listée ici est celle adaptée à la version de Frama-C du Cremi (Sulfur). Vous pouvez depuis le site de Frama-C consulter des versions plus récentes (ou anciennes).

• Le site de Frama-C.
• Documentation pour ACSL (notamment pour la syntaxe).
• Manuel du module WP.
• Manuel du module RTE.
• ACSL by Example. Un livre donnant des exemples (par difficulté croissante) d’algorithmes spécifiés et vérifiés avec Frama-c.

Le Cours (version encore incomplète). Version avec open-dyslexic

Comment installer frama-c chez vous.

Sujets et bases de codes d’exercices:

• TP1 - Prise en main de Frama-C. Version pdf. Version open-dyslexic (pdf). Archive contenant les sources.
• TP2 - Pointeurs. Version pdf. Version open-dyslexic (pdf). Archive contenant les sources.
• TP3 - Boucles. Version pdf. Version open-dyslexic (pdf). Archive contenant les sources.
• TP4 - Terminaison. Version pdf. Version open-dyslexic (pdf).Archive contenant les sources.
• TP5 - Fonctions logiques et prédicats. Version pdf. Version open-dyslexic (pdf).Archive contenant les sources.

• TD1 - Weakest Precondition simple. Et les sources pour pouvoir composer.
• TD2 - Un programme avec boucle annoté. Et les sources pour pouvoir composer.
• TD3 - Un programme avec boucle sans annotations. Et les sources pour pouvoir composer.
• TD-TP - devoir maison à rendre. Et les sources pour composer et coder.