Courses/IMC

Titre	Introduction au Model checking
Sigle	IMC
Enseignant	Alexandre Duret-Lutz
Période	S5, Ing3
Public	Majeure, CSI"CSI" is not in the list (InfoSup, InfoSpé, Tronc-commun, Majeure, Apprentis, Cycle Ing, SCIA, AppIng, RDI, IMAGE, ...) of allowed values for the "Course audience" property.
Contrôle
Durée
Optionnel	non
Module	Sciences Générales
Prérequis	ALGO
Objectifs	Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets.
Plan	Introduction de la vérification formelle et du model checking Diagrammes de décision binaires (BDD) Logique temporelle à temps arborescent (CTL) et vérification à l'aide de BDD Diagrammes de décision hiérarchiques (SDD) Logique temporelle à temps linéaire (LTL) et passage vers les automates de Büchi Test de vacuité d'un automate de Büchi Lutte contre l'explosion combinatoire de l'espace d'état Hypothèses d'équité et automates de Streett Introduction à Spin.
Documentation	Model Checking. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. MIT Press. The Spin Model Checker: Primer and Reference Manual. Gerard J. Holzmann. Addison-Wesley.
Support	FIXME : http://www.lrde.epita.fr/cgi-bin/twiki/view/Epita/IMC-Course.
Journaux