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

Basics of Verification (60h, 7 ECTS)

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

Lecturers in 2020—2021

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 (this year)

The first lecture will start on Friday 18/09 at 10am.

Date Topics covered Documents
2020/09/18 Introduction & motivation
Models: Transition systems (Kripke structures), variables, synchronized products, Rendez-vous,
shared variables, atomicity, asynchronous communication, FIFO channels
Slides
2020/09/25 Specification: introduction, examples, temporal structures, first-order vs temporal logics
Linear temporal logics: definitions, examples, model checking
Slides
2020/10/02 linear vs branching specifications, Branching specifications.
MSO, CTL*, CTL: definitions, examples, model checking
Slides
2020/10/09 PTIME Model checking algorithm for CTL Slides
2020/10/16 PTIME Model checking algorithm for CTL with fairness
Büchi automata: definition, examples, main properties, generalized acceptance, unambiguity
Slides
2020/10/23 Sequential Büchi transducers: definition and examples
Sequential Büchi transducer for basic LTL formulas
Construction of a sequential Büchi transducer for an arbitrary LTL formula
Slides
2020/11/06 Satisfiability and Model checking for LTL in PSPACE: decision procedure and hardness
PSPACE model checking algorithm for CTL*
Slides

Detailed description and Lecture notes (last year)

Date Topics covered Documents
2019/11/15 Büchi emptiness check Slides
2019/11/22 Partial-order reduction Slides
2019/11/29 Binary decision diagrams Slides
2019/12/06 Petri nets Slides
Homework10
Exercises
2019/12/13 Petri nets Slides
Homework11
Exercises
2019/12/20 Petri nets, Pushdown systems Slides
Homework12
Exercises
2020/01/10 Abstraction/refinement Slides
Homework9
Exercises

Exams

Mid-term exam 2019-2020: questions and answers

Previous years's questions for mid-term exams: 2018-2019 2017-2018 2016-2017 questions, 2016-2017 with answers, 2015-2016, 2014-2015.

Final exams 2016-2017: questions, answers

Final exams 2017-2018: questions, answers

Prerequisites

Finite Automata
First-order logic

Related courses

Bibliography

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

Teachers

Paul GastinPRENS Paris-SaclayLSV
Stefan SchwoonMCENS Paris-SaclayLSV
Nathan ThomassetPhDENS Paris-SaclayLSV

Previous Years

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