The default language is French.
But the lectures may be given in English if attended by non French-speaking students.
Nowadays, it is of the highest importance to use formal methods in order to increase the reliability of critical systems.
In this introductory course on verification of discrete systems, we concentrate in particular on model checking techniques.
We will describe various models used to define systems: transition systems enriched with various data structures (variables, channels, ...) and which can be composed with several synchronization mechanisms.
We will also cover specification languages that are used to express properties to be checked on our systems: temporal logics (linear or branching), first-order or monadic second-order logic, ...
We will study expressivity, decidability and complexity properties of our models and specification languages.
We will also cover abstraction/refinement techniques and (bi)simulation relations used to relate various abstraction levels.
Algorithmic aspects of model checking will be investigated and we will stress efficient techniques such as binary decision diagrams (BDDs) or bounded model checking.
Here are some rough notes covering most of the first half.
Here are the planned contents for the first half of the course (which might change slightly):
| Date | Topics covered |
| 2015/09/15 | Introduction & motivation slides
Finite-state models: transition systems
Temporal frames: modal logic, first-order logic |
| 2015/09/22 | Branching time: CTL model-checking
CTL*, fair CTL, CTL+ |
| 2015/09/29 | Linear time: LTL
Büchi automata (BA) |
| 2015/10/06 | very weak alternating Büchi automata (vwABA)
translation from LTL to vwABA to BA |
| 2015/10/13 | Upper bounds: PSPACE-easiness of LTL and CTL* model-checking |
| 2015/10/20 | Lower bounds: PSPACE-hardness of LTL and CTL* model-checking |
| 2015/11/03 | High-level models
SPIN |
| 2015/11/24 | Lecture (Depth-First Search, Partial-Order Reduction) |
| 2015/12/01 | Lecture (Partial-Order Reduction, Binary Decision Diagrams) |
| 2015/12/08 | Lecture (Binary Decision Diagrams, Abstraction/Refinement) |
| 2015/12/15 | Lecture (Abstraction/Refinement, Bounded Model-Checking) |
| 2016/01/05 | Lecture (Petri nets, preliminary slides) |
There will be 2 written exams (E1 and E2) and 2 home assignments (H1 and H2).
The final mark will be (H1+2E1+H2+2E2)/6.
The examination questions will be in French and/or in English depending on the requests.
Students may write their answers in French or in English.
Finite Automata
First-order logic
Principles of Model Checking. Christel Baier and Joost-Pieter Katoen.
MIT Press, 2008.
Systems and Software Verification. Model-Checking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen. Springer, 2001.
Also available in french: Vérification de logiciels : Techniques et outils du model checking. Coordonné par Ph. Schnoebelen. Vuibert, 1999.
Model Checking. E.M. Clarke, O. Grumberg, D. Peled.
MIT Press, 1999.
Temporal Verification of Reactive Systems - Safety. Zohar Manna and Amir Pnueli. Springer-Verlag, 1995.
The Temporal Logic of Reactive and Concurrent Systems - Specification. Zohar Manna and Amir Pnueli. Springer-Verlag, 1992.
| Sylvain Schmitz | MC | ENS Cachan | LSV |
| Thomas Chatain | MC | ENS Cachan | LSV |
| Stefan Schwoon | MC | ENS Cachan | LSV |
| Daniel Stan | PhD | ENS Cachan | LSV |