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

Basics of Verification (48h, 6 ECTS)

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


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


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

The full lecture notes of the first half of the semester are available here.

Date Type Topics covered
2012/09/19 Lecture Introduction
Models: transition systems, variables, synchronized products, Rendez-vous, shared variables, atomicity, asynchronous communication with channels
2012/09/26 Exercises Mutual exclusion algorithms, Handshake with data exchange, Needham-Schroeder protocol, Channel systems
2012/10/03 Lecture Specification: introduction, linear vs branching specifications, FO and TL: definitions and examples, linear model checking, branching specifications, MSO, CTL*
2012/10/10 Exercises Temporal Logics: LTL, CTL*, CTL, CTL+
2012/10/17 Lecture CTL, PTIME model checking algorithm for CTL and for fair-CTL
Büchi automata
2012/10/24 Exercises CTL model-checking, Büchi automata
2012/10/31 Lecture Büchi transducers: definitions, examples and main properties
Construction of a Büchi transducer from an LTL formula
Satisfiability and Model checking for LTL: decidability and complexity
PSPACE model checking algorithm for CTL*
2012/11/07 Exercises LTL model-checking and complexity
2012/11/14 Lecture Temporal logics: Expressivity, Ehrenfeucht-Fraïssé games, Separation
2012/11/21 Exercises EF Games, Separation
2012/12/13 Lecture Petri Nets I
2012/12/19 Exercises Petri nets: model-checking, unfoldings, VASS
2013/01/09 Lecture Petri Nets II
2013/01/16 Exercises Coverability
2013/01/23 Lecture Binary Decision Diagrams
2013/01/30 Exercises BDDs
2013/02/06 Lecture Pushdown systems
2013/02/13 Exercises Pushdown systems
2013/02/20 Lecture Partial-order reduction
2013/02/27 Exercises Parial-order reduction

See also previous year.


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
2012/10/24 H1: Alternation-Free Mu-Calculus To hand in on November 7th.
Don't be late.
2012/11/28 E1: Exam on the first half of the course.
2013/01/30 H2: Fairness and Petri Nets To hand in on February 13th17th.
Some sketches of answers.
2013/03/06 E2: Exam questions, sample solutions Exam on the second half of the course.


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.


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


Paul GastinPUENS CachanLSV
Sylvain SchmitzMCENS CachanLSV
Stefan SchwoonMCENS 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