In charge: Étienne Lozes and 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.
Lecture Notes of Etienne Lozes (very unstable version, will be updated regularly). Please do not hesitate to send me your comments.
| Date | Topics covered |
|---|---|
| 2014/09/16 | Introduction Models: transition systems, variables, synchronized products, rendez-vous Slides Specification: introduction, linear vs branching specifications, FO and TL: definitions and examples, linear model checking, branching specifications, MSO, CTL* |
| 2014/09/23 | … Mutual exclusion algorithms, Handshake with data exchange, Needham-Schroeder protocol |
| 2014/09/30 | mu-calculus… CTL, PTIME model checking algorithm for CTL |
| 2014/10/07 | mu-calculus… CTL+ |
| 2014/10/14 | Büchi automata… CTL PTIME-complete, fair CTL Slides |
| 2014/11/18 | Emptiness test for Büchi automata (Slides) Binary decision diagrams (Slides) |
| 2014/12/02 | Partial-order reduction (Slides) |
| 2014/12/09 | Petri nets part 1 (Slides) |
| 2014/12/16 | Petri nets part 2 (Slides) Abstraction/refinement (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.
Since the second homework did not take place, the final mark will be (H1+2E1+2E2)/5.
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.
| Date | Type | Topics and comments |
|---|---|---|
| 2014/11/10 | E1: midterm exam | Exam on the first half of the course. |
| 2015/01/13 | E2: final exam, solutions | Exam on the second half of the course. |
Concerning the second part of the course, the exams and solutions of previous years can be found in the pages for previous editions of the course (see the links at the bottom of the page), except for 2013-14, which are here (exam) and here (solutions).
Finite Automata.
| Étienne Lozes | MC | ENS Cachan | LSV |
| Thomas Chatain | MC | ENS Cachan | LSV |
| Stefan Schwoon | MC | ENS Cachan | LSV |
| Daniel Stan | PhD | ENS Cachan | LSV |