INFO4212 : Sémantique et vérification
Semantics and verification
- Responsable(s) :
-
- Daniel Hirschkoff
- Enseignant(s) :
-
- Colin Riba
Niveau
M1+M2
Discipline
Informatique
ECTS
3.00
Période
2e semestre
Département
Localisation
Site Monod
Année
2024
Public externe (ouverts aux auditeurs de cours)
Informations générales sur le cours : INFO4212
Content objectif
The goal of formal verification is to check automatically that some programs or systems
are correct with respect to their requirements.
In this course we present mathematical models of programs and systems and we
describe classes of properties which can be automatically checked on these models.
Content of the course:
- Modelling with Labelled Transition Systems
- Linear-Time Properties
- Definition and Examples
- Characterizations via Order Theory and Topology
- Linear Temporal Logic
- ω-Regular Properties and Büchi Automata
- Bisimulation and Modal Logic
- Bisimulation and Trace Equivalence
- Hennessy-Milner Logic
- Bisimulation and Logical Equivalence
Content prerequis
Prerequisites from the L3 year of the Computer Science Department of ENS de Lyon:
- Fondements de l'informatique.
- Logique.
Content bibliographie
- Course notes (regularly updated).
- The course is mostly based on the book:
- Baier, C. and Katoen, J.-P., Principles of Model Checking, MIT Press, 2008.