
This is an old revision of the document!
The default language is French.
But the lectures may be given in English if attended by non Frenchspeaking 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), firstorder or monadic secondorder 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.
Detailed description and Lecture notes
Date  Topics covered  Documents 
2017/09/14  Introduction & motivation
Models: Transition systems (Kripke structures), variables, synchronized products, Rendezvous,
shared variables, atomicity, asynchronous communication, FIFO channels  Slides
Homework1
Exercises 
2017/09/21  Specification: introduction, linear vs branching specifications, firstorder vs temporal logics
Linear temporal logics: definitions, examples, model checking  Slides
Homework2
Exercises 
2017/09/28  Branching specifications, MSO, CTL^{*}, CTL: definitions, examples, model checking  Slides
Homework3
Exercises 
2017/10/05  PTIME Model checking algorithm for CTL and for CTL with fairness
Büchi automata: definition and first examples  Slides
Homework4
Exercises 
2017/10/12  Büchi automata: main properties, generalized acceptance, unambiguity
Sequential Büchi transducers: definition and examples
Sequential Büchi transducer for basic LTL formulas  Slides
Homework5
Exercises 
2017/10/19  Construction of a sequential Büchi transducer for an arbitrary LTL formula
Satisfiability and Model checking for LTL: decidability and complexity
PSPACE model checking algorithm for CTL^{*}  Slides
Homework6
Exercises 
2017/10/26  Temporal logics: Expressivity, EhrenfeuchtFraïssé games, Separation  Slides 
2017/11/09  Büchi emptiness check  Slides
Exercises 
2017/11/16  Partialorder reduction  Slides
Homework7
Exercises 
2017/11/23  Pushdown systems  Slides
Exercises 
2017/11/30  Binary decision diagrams  Slides
Homework8
Exercises 
2017/12/07  Abstraction/refinement  Slides
Homework9
Exercises 
2017/12/14  Petri nets  Slides
Homework10
Exercises 
2017/12/21  Petri nets  Slides
Homework11 
Finite Automata
Firstorder logic

Principles of Model Checking. Christel Baier and JoostPieter Katoen. MIT Press, 2008.
Systems and Software Verification. ModelChecking 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. SpringerVerlag, 1995.
The Temporal Logic of Reactive and Concurrent Systems  Specification. Zohar Manna and Amir Pnueli. SpringerVerlag, 1992.
Paul Gastin  PR  ENS ParisSaclay  LSV 
Stefan Schwoon  MC  ENS ParisSaclay  LSV 
Marie Fortin  PhD  ENS ParisSaclay  LSV 
