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