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 :  lundi 16 janvier,  lundi 23 janvier et lundi 30 janvier, de 14h00 à  17h15. Chaque séance dure 3h00.

Contrôle continu :  oui (pour ma partie : petit projet sur le model checker Spin)




Plannig et Contenu




Liste des devoirs maison


pas de devoir maison


Back