Formal verification of computer systems

• Introduction : notion de spécification et de vérification formelles.
• Systèmes à transitions labellées, automates, et logiques temporelles (LTL et CTL).
• Propriété de sûreté et de vivacité.
• Equivalence de comportement et réductions.
• Automates temporisé.
• Chaines de Markov et processus de décision Markoviens.

Etude des techniques et outils existants pour spécifier et vérifier formellement des systèmes réactifs.

Connaissances et compétences pré-requises ou co-requises

-éléments de logique
-éléments de théorie des automates

Cours ayant celui-ci comme co-requis

Cours ex-cathedra et séminaires de mise en pratique

Références, bibliographie et lectures recommandées

Clarcke, E., O. Grumberg et D. Peled, 1999. Model Checking. - MIT Press.
C. Baier and J.-P. Katoen. Principles of Model Checking, 2008 - MIT Press.

Support(s) de cours

• Université virtuelle
• Syllabus

Informations complémentaires

Slides distribués aux étudiants via UV.

Contacts

Jean-François Raskin (jraskin@ulb.ac.be)

Campus

Plaine

Méthode(s) d'évaluation

• Autre

Autre

Examen écrit.

Construction de la note (en ce compris, la pondération des notes partielles)

Examen écrit.

Langue(s) d'évaluation

• anglais