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 2015—2016


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 some rough notes covering most of the first half.

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

Date Topics covered
2015/09/15 Introduction & motivation slides
Finite-state models: transition systems
Temporal frames: modal logic, first-order logic
2015/09/22 Branching time: CTL model-checking
CTL*, fair CTL, CTL+
2015/09/29 Linear time: LTL
Büchi automata (BA)
2015/10/06 very weak alternating Büchi automata (vwABA)
translation from LTL to vwABA to BA
2015/10/13 Upper bounds: PSPACE-easiness of LTL and CTL* model-checking
2015/10/20 Lower bounds: PSPACE-hardness of LTL and CTL* model-checking
2015/11/03 High-level models
2015/11/24 Lecture (Depth-First Search, Partial-Order Reduction)
2015/12/01 Lecture (Partial-Order Reduction, Binary Decision Diagrams)
2015/12/08 Lecture (Binary Decision Diagrams, Abstraction/Refinement)
2015/12/15 Lecture (Abstraction/Refinement, Bounded Model-Checking)
2016/01/05 Lecture (Petri nets, preliminary 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.

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
2015/09/29 H1: First-order logic with 2 variables To hand in on October 13th.
Don't be late.
2015/12/17 H2: Symmetric Model Checking To hand in on January 5th 2015.
2016/01/12 E2: final exam Exam on the second half of the course, room C509, 9h-11h


Finite Automata
First-order logic

Related courses


  • 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.


Sylvain SchmitzMCENS CachanLSV
Thomas ChatainMCENS CachanLSV
Stefan SchwoonMCENS CachanLSV
Daniel StanPhDENS 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