Stephan Merz : Vérification algorithmique 2005/06

Vérification algorithmique

(Olivier Bournez et Stephan Merz)

Les documents disponibles ici concernent la première partie du cours traitant des notions élémentaires de la vérification algorithmique et des logiques temporelles (cette partie est commune aux filières IL et ML du master informatique).

Annonces

Le mini-projet sur la vérification d'un ascenseur (voir énoncé) est à rendre pour le 4 novembre 2005 (pour les étudiants en filière IL).

Il n'y a pas de TD lundi 17 octobre. Les suivants (et derniers) TD auront lieu le 24 octobre.

La deuxième partie du cours (pour la filière ML) sera assurée par Olivier Bournez. Elle commencera le jeudi 20 octobre.

Heures de cours


  jeudi        10h  - 12h     Amphi 6
  vendredi     14h  - 16h     Amphi 6
  lundi        8h30 - 12h30   E33        (TD)

Les travaux dirigés sont obligatoires pour les étudiants inscrits en master professionel (filière IL) mais ouverts à tous.

Documents

toutes les polycopies en un seul fichier (PDF)
28/09/2005: [ transparents | protocole de Lynch ]
05/10/2005: [ transparents ]
06/10/2005: [ transparents ]
12/10/2005: [ transparents ]
13/10/2005: [ transparents ]
19/10/2005: [ transparents ]
TD 04/10/2005: [ énoncé | sémaphore en Spin | propriétés LTL ]
TD 10/10/2005: [ énoncé | modèle de l'ascenseur ]
TD 24/10/2005: [ énoncé ]
02/12/2005: [ examen filière IL (exercices 2 et 3) ]

Quelques liens

Spin model checker (voir aussi les références Promela)
NuSMV (model checking symbolique pour LTL et CTL)
Vérificateur Murphi

Quelques références bibliographiques

B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen:: Systems and Software Verification. Model Checking Techniques and Tools. Springer Verlag, 2001.
Version française (1999)
Edmund M. Clarke, Orna Grumberg, Doron Peled:: Model Checking. MIT Press, 1999
Edmund M. Clarke, Holger Schlingloff:: Model Checking. Chapter 21 in Alan Robinson and Andrei Voronkov (eds.), Handbook of Automated Reasoning, Elsevier Science Publishers B.V., pp. 1367 - 1522 (2000) [ps.gz]
Michael Huth, Mark D. Ryan:: Logic in Computer Science. Cambridge University Press, 2004 (2nd edition).
Stephan Merz:: Model Checking: A Tutorial Overview. In: F. Cassez et al. (eds.): Modeling and Verification of Parallel Processes, pp. 3 - 38. Lecture Notes in Computer Science 2067, Springer Verlag 2001. [pdf]

Stephan Merz