Cours de Software Model Checking, M2, UPSaclay

Ce cours est une introduction au Model checking, une technique de pointe en vérification automatique. Nous ferons un tour d'horizon des bases de la méthode [systèmes réactifs et modélisation, propriétés d'accessibilité / invariance / sûreté, logiques temporelles LTL / CTL / CTL*, algorithmesde model checking pour CTL (par marquage) et LTL (par automates), algorithmes efficaces] avant d'aborder les travaux récents de software model checking. Le cours est donné au M2 FIIL de l'Université Paris-Saclay, avec Fatiha Zaidi et Sylvain Conchon.

Organisation

Lieu et horaires : les 3 cours ont lieu les jours suivants : mercredi 8 janvier, lundi 13 janvier et mercredi 15 janvier, de 14h00 à 17h15 (salles D201/D103 ou E105/E202). Chaque séance dure 3h00.

Contrôle continu : non

Plannig et Contenu

Séance 1 (08/01/2020) : logiques temporelles, algorithmes de model checking, TD2, TD3 [poly de cours (couvre juste le début du cours)]
Séance 2 (13/01/2020) : suite algorithmes et model checking efficace
Séance 3 (15/01/2020) : software model checking, TP Spin

Liste des devoirs maison

pas de devoir maison

Back