Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Basics of Verification (60h, 6 ECTS)

In charge: Stefan Schwoon (LSV, ENS Cachan).

Lecturers in 2016—2017


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

Here are the planned contents for the first half of the course (which might change slightly):

Date Topics covered
2016/09/15 Introduction & motivation slides
Finite-state models: Kripke structures, LTL
2016/09/22 CTL*, CTL
2016/09/29 CTL, fair CTL, CTL+
2016/10/06 Büchi automata
2016/10/13 LTL model-checking
2016/10/20 CTL* model-checking, CTL model-checking PTIME-complete
2016/11/17 Büchi emptiness check, Partial-order reduction
2016/11/24 Partial-order reduction and Binary decision diagrams
2016/12/01 Binary decision diagrams
2016/12/08 BDDs and Abstraction/refinement
2016/12/15 Abstraction and Petri nets
2017/01/05 Petri nets
2017/01/12 Exam 14h-16h


This years's mid-term exam: subject, with solutions.

Final exam: subject, solutions

Last years's subjects for mid-term exams: 2015, 2014.


Finite Automata
First-order logic

Related courses


  • Ph. Schnoebelen. The Complexity of Temporal Logic Model Checking. In AiML’02, pages 393-436. King’s College Publication, 2003. Invited paper.
  • 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.


Philippe SchnoebelenDRCNRSLSV
Thomas ChatainMCENS CachanLSV
Stefan SchwoonMCENS CachanLSV
Marie FortinPhDENS CachanLSV

Previous Years

Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA