In charge: Stefan Schwoon (LSV, ENS Cachan).
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.
| Date | Topics covered | Documents |
|---|---|---|
| 2018/09/20 | Introduction & motivation Models: Transition systems (Kripke structures), variables, synchronized products, Rendez-vous, shared variables, atomicity, asynchronous communication, FIFO channels | Slides Homework1 Exercises |
| 2018/09/27 | Specification: introduction, linear vs branching specifications, first-order vs temporal logics Linear temporal logics: definitions, examples, model checking | Slides Homework2 Exercises |
| 2018/10/04 | Branching specifications, MSO, CTL*, CTL: definitions, examples, model checking | Slides Homework3 Exercises |
| 2018/10/11 | PTIME Model checking algorithm for CTL and for CTL with fairness Büchi automata: definition and first examples | Slides Homework4 Exercises |
| 2018/10/18 | Büchi automata: main properties, generalized acceptance, unambiguity Sequential Büchi transducers: definition and examples Sequential Büchi transducer for basic LTL formulas Construction of a sequential Büchi transducer for an arbitrary LTL formula | Slides Homework5 Exercises |
| 2018/10/25 | Satisfiability and Model checking for LTL: decidability and complexity PSPACE model checking algorithm for CTL* Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation | Slides Homework6 Exercises |
| 2018/11/15 | Büchi emptiness check | Slides Homework7 Exercises |
| 2018/11/22 | Partial-order reduction | Slides Homework8 Exercises |
| 2018/11/29 | Binary decision diagrams | Slides Homework9 Exercises |
| 2018/12/06 | Petri nets | Slides Homework10 Exercises |
| 2018/12/13 | Petri nets | Slides Homework11 Exercises |
| 2018/12/20 | Petri nets, Pushdown systems | Slides Homework12 Exercises |
| 2019/01/10 | Pushdown systems, Abstraction/refinement | Slides Homework9 Exercises |
This years's mid-term exam:
Final exam: January 17, 2019, 14h-16h. All course materials can be used.
Last years's subjects for mid-term exams: 2017 subject 2016 subject, 2016 with solutions, 2015, 2014.
Finite Automata
First-order logic
| Paul Gastin | PR | ENS Paris-Saclay | LSV |
| Stefan Schwoon | MC | ENS Paris-Saclay | LSV |
| Marie Fortin | PhD | ENS Paris-Saclay | LSV |