Master Informatique - Université de Bordeaux

Responsables : Alain Griffault et Vincent Penelle

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

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

Partie 2 (Vincent Penelle) : 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 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).