Sémantique et Vérification
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 systemsand 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
- ω-Regular Properties and Büchi Automata
- Linear Temporal Logic
- Bisimulation and Modal Logic
- Bisimulation and Trace Equivalence
- Hennessy-Milner Logic
- Bisimulation and Logical Equivalence
The course follows parts of the book: Baier, C. and Katoen, J.-P., Principles of Model Checking, MIT Press, 2008.
We assume some familiarity with automata theory and mathematical logic, essentially
corresponding to the courses Fondements de l’informatique and Logique given in the
L3 year of the Computer Science Department of the ENS de Lyon.