Cours de Model Checking, M1, ENSTA

*** cours donnés à l'ENSTA et à l'Ecole Polytechnique ***

*** je donne une version remaniée du cours à l'Université Paris-Saclay ***

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* et algorithmes de model checking pour CTL (par marquage) et LTL (par automates).

poly complet du cours
slides introduction, TD1
slides logiques temporelles , TD2
slides algo de model checking-1 , slides algorithmes de model checking-2 , TD3

Back