Master Informatique - Université de Bordeaux

Cette page est en lecture seule. Vous pouvez afficher le texte source, mais ne pourrez pas le modifier. Contactez votre administrateur si vous pensez qu'il s'agit d'une erreur.

====Conception Formelle====

Responsables : [[https://dept-info.labri.fr/~griffaul/| Alain Griffault]] et [[https://labri.fr/perso/vpenelle | Vincent Penelle]]

Ce cours du S8 est commun avec le parcours GL. Il vaut 6ECTS.

===Résumé===

Partie 1 (Alain Griffault) : Alta-rica (todo).

Partie 2 (Vincent Penelle) : 
[[https://www.labri.fr/perso/vpenelle/Enseignement/ConceptionFormelle/|Page de ressources]]

Cette partie du cours est consacrée à la spécification et la vérification de programmes en C grâce à la technique de calcul de Weakest Precondition, et fait pratiquer cette technique grâce au logiciel [[https://www.frama-c.com|Frama-C]].
Le cours présente les bases théorique du calcul de Weakest Precondition. Il apprend également à spécifier des contrats de fonctions en logique du premier ordre. Le logiciel Frama-C accepte de telles spécification (avec une syntaxe équivalent à la logique du premier-ordre).

Master Informatique - Université de Bordeaux

Outils pour utilisateurs

Outils du site

Outils de la page