Méthodes formelles - M2 MIC (2018--2019)
Equipe enseignante
François Laroussinie et Arnaud Sangnier.
Actualités
Le premier cours aura lieu VENDREDI 11 JANVIER à 9h45 en salle 2004 (bâtiment Sophie Germain).
Documents
Transparents du cours du 11 janvier
(introduction, structures de Kripke, LTL).
TD sur LTL
.
Modèle Prism pour le TD1
.
Modèle de l'algorithme de Peterson (V1)
.
Propriétés de l'algorithme de Peterson
.
Description du distributeur de tickets de train
.
Modèle PRISM du distributeur de tickets
.
Transparents du cours du 18 janvier
(spécification d'un ascenseur).
Transparents du cours du 25 janvier
(algorithme pour LTL).
Transparents du cours du 1er février
(CTL).
TD du 1er février
.
Suite des transparents du cours du 1er février
(model-checking de CTL).
Email:
francois.laroussinie[at]univ-paris-diderot.fr