Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

[Home page]

[How to contact us]
[How to apply]
[Entrance requirements]
[Management]

[The MPRI course]

[Organisation]
[Standard courses]
[Level 1 modules]
[Level 2 modules]
[Teaching staff]

[Practical information]

[Calendar and timetable]
[Student directory]
[Examinations calendar]
[Internships]
[Scolarships]

Basics of Verification (48h, 6 ECTS)

In charge: Paul Gastin (LSV, ENS Cachan).

Lecturers for 2009-2010

Paul Gastin (lectures), Stefan Schwoon (lectures), Sylvain Schmitz (exercises).

Research internships

Language

The default language is French.
But the lectures may be given in English if attended by non French-speaking students.

Motivations and main objectives

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.

Detailed description and Lecture notes

Date	Type	Topics covered
09/14	Lecture	Introduction, Models: transition systems, variables, synchronized products, Rendez-vous slides Specification: introduction, LTL: definitions and examples slides
09/21	Exercises	Handshake with data exchange, Needham-Schroeder protocol LTL formulae Büchi automata
09/28	Lecture	Models: shared variables, atomicity, (lossy) channels LTL: past modalities, expressivity, model checking, satisfiability Büchi automata
10/05	Exercises	Alternating Bit Protocol LTL with Past Büchi Complementation
10/12	Lecture	Efficient construction of a Büchi automaton from an LTL formula Correctness of the construction. Satisfiability and Model Checking are PSPACE-complete for LTL specifications (upper bound and lower bound)
10/19	Exercises	LTL to Büchi Automata Suttering and LTL(U) Lower bounds for LTL(U)
10/26	Lecture	Branching time specifications PSPACE model checking algorithm for CTL^* PTIME model checking algorithm for CTL Fair CTL and its PTIME model checking algorithm
11/02	Exercises	Model Checking a Path CTL^*, CTL, and CTL⁺ Fair CTL
11/09	Simple exercises in preparation for E1	LTL and Automata CTL and CTL^* Model checking LTL(X) is NP-complete
11/23	Lecture	Binary decision diagrams: introduction, operations, use in CTL and LTL model checking
11/30	Exercises	Binary decision diagrams
12/07	Lecture	(Bi-)simulation relations, abstraction refinement
12/14	Exercises	(Bi-)simulation Quotienting Existential CTL equivalence
01/04	Lecture (part 1, part 2)	Bounded model checking, Petri nets
01/11	Exercises	Modeling with Petri nets LTL model checking for Petri nets Coverability, Rackoff's algorithm
01/18	Lecture	Petri nets
01/25	Exercises	Vector Addition Systems Unfoldings: Adequate Partial Orders, LTL Model Checking

Exams

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.

Date	Type	Topics covered
10/12	H1: Home assignment to hand in before or on 10/26 a few partial answers	Mutual Exclusion Cantor Topology on Σ^ω Decomposition into Safety and Liveness Separation of LTL Formulae into Past and Future Characteristic Safety/Liveness Formulae Model Checking Safety Properties
11/16	E1: from 12:45 to 15:45. The only authorized documents are the lecture notes Examination questions and solutions	All topics covered during the first half of the semester
12/14	H2: Home assignment to hand in before or on 2010/01/11 a few partial answers	Stutter Bisimulation CTL^*(U) equivalence
2/8	E2: from 12:45 to 15:45. The only authorized documents are the lecture notes (of the entire course). Exam and solutions	All topics covered during the semester, especially the second half

Prerequisites

Finite Automata.

Related courses

1-2: Automates avancés et applications
1-18: Automates d'arbres et applications
2-8: Fondements pour la vérification des systèmes temps-réel
2-9: Vérification de systèmes dynamiques et paramétrés
2-16: Modélisation par automates finis
2-20-1: Jeux pour la théorie des automates, la vérification et l'internet.

Bibliography

Principles of Model Checking. Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.
Vérification de logiciels : Techniques et outils du model checking. Livre collectif 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.

Teachers

Paul Gastin	PU	ENS Cachan	LSV
Sylvain Schmitz	MC	ENS Cachan	LSV
Stefan Schwoon	MC	ENS Cachan	LSV

Previous years

* 2008-2009

Les années précédentes

* Année 2009-2010