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

Verification of dynamic and parameterized systems (48h, 6 ECTS)

People in charge : Finkel (LSV, ENS de Cachan), responsible for this year, and, Ahmed Bouajjani (LIAFA, Univ. Paris 7) and, Philippe Schnoebelen (LSV, ENS de Cachan).

The lectures take place on Tuesday from 16h15 until 18h45 at the Chevaleret building (room 1E01).


Motivation and goals of the course

Since 1990, the algorithmic techniques for the verification of systems are used increasingly in industry and are capable of taking into account more and more aspects of systems. The course 2-9 presents certain recent advances in the domain ofautomatic verification by model-checking, in particular concerning the verification of models with an infinite (unbounded) number of configurations, allowing to analyse and validate dynamic and parameterized complex systems like embedded systems, distributed algorithms, modern telecommunication protocols, etc.

The basic tool used in this course arecounter machines which represent a fundamental theoretical model. Therefore, the course presents some classical results which are of general interest going beyond the subject of automatic verification. For example, we study Presburger logic, undecidability of Minsky machines, etc.

Language of the course

The course will be taught in English since at least two foreign students requested it during the first class (Sep. 13th). The exams will be given in English (it is okay to answer in French).

Prerequisites & neighbouring courses

To follow the course 2-9 a student should have some basic notions in computability and complexity theory, in logique and should master the basic concepts of finite automata theory and regular languages.

The course 2-9 is a quite natural follow-up of the course 1-22 which is giving a general introduction to the domain of verification. However, it is not necessary to have followed course 1-22.

The courses 2-6 (on abstract interpretation and application to verification and static analysis) , 2-8 (on the verification of timed, hybrid and concurrent systems: it introduces a similar scientific approach but concentrates on timed aspects), 2-36-1 about proof of programs, 2-7-2 about proof-assistants and 2-20-1 about games theory are all intetresting complements of course 2-9.

Contents of the course

Part I : Counter machines and well orderings: Monotone Counter Machines

Course Date Teacher Contents References Lecture notes and exercises
2-9.1 13 sep A. Finkel Introduction. Counter machines: A fundamental model for modelling and verifying programs and systems.
Examples of modelling: SyracuseProblem, Broadcast protocols, Programs for list manipulation, ...
A recent but uncomplete proof of the Syracuse problem
presentation course 2-9;
Exercise: what are the reachable configurations for the 3 counter machine in the Feb. 2009 exam?
2-9.2 20 sep A. Finkel On families of counter machines: relational, fonctional, affine, linear, translations, Minsky machines (called initially register machines), vector addition systems (VAS) and Petri Nets. Undecidability of the termination and reachability problems for Minsky machines. Decidability for VAS. Relational, functional and affine CMs [DFGD'2010] slides-2nd-lecture
Exercises lectures 1 - 2 to send before 26 september
2-9.3 27 sep A. Finkel Definition of well-quasi-orderings (also called WQO). Dickson's lemma and Higman's lemma. Well-structured transition systems (WSTS). Examples of well-structured (or not) extended VAS. Decidability of the termination and the finiteness problems of well-structured transition systems(WSTS).Computability of predecessor sets Pre^*(X). [FS01], [Kru72] slides-3rd-lecture
2-9.4 4 oct A. Finkel Monotonic (aka well-structured) counter machines. Decidability of reachability & safety, termination. Computability of predecessor sets Pre^*(X). Undecidability of Büchi properties, of finiteness. slides-4th-lecture
notes-monotonic CM;
Undecidability for reset
2-9.5 11 oct A. Finkel The computation of the cover for monotonic counter machines. Applications for solving decidability of various problems. Open problems for research. [FG'09]

Partie II : Monotone Games in Counter systems

Course Date Teacher Contents References Lecture notes
2-9.6 18 oct Laurent Doyen Reminder of two-player graph games with reachability and safety objectives. Monotonic games. General results of decidability and undecidability. [ABO'03] [1]
2-9.7 25 oct Laurent Doyen Energy games. Definition, computational complexity, strategy complexity. Algorithm. [BFLMS'08]
2-9 1er nov pas de cours
2-9.8 8 nov Laurent Doyen Energy games with partial observation. Finite memory strategies. Decidability and undecidability results. [DDGRT'10] [4]
2-9.9 15 nov Laurent Doyen Energy parity games. Special case of energy Buechi and energy coBuechi games. Memory requirement and computational complexity. [CD'10] [5]
2-9.10 22 nov Laurent Doyen Multi-counter games. Generalized energy games. Strategy complexity and computational complexity. [CDHR'10]
2-9 29 nov Mid-term exam

Partie III : Counter systems and Presburger arithmetic

Course Date Teacher Contents References Lecture notes
2-9.6 6 dec P. Habermehl Presburger arithmetic. Decidability by the quantifier elimination method. Slides
2-9.7 13 dec P. Habermehl Lower-bound for the complexity of Presburger arithmetic [FR74] Slides
2-9.8 20 dec Pas de cours
2-9.8 3 jan P. Habermehl Decidability using finite-state automata. Slides
2-9.9 10 jan P. Habermehl Extension to real numbers using weak Büchi automata. Slides
2-9.10 17 jan P. Habermehl Presburger definable sets = semilinear sets. Applications. Slides

Part IV : Modelling and verification of programs using Presburger

Course Date Teacher Contents Biblio Lecture notes
2-9.16 24 jan A. Sangnier Reachability in functional flat counter systems, flattable counter systems [FL02] [LS05][HP79]
2-9.17 31 jan A. Sangnier Reachability in relational flat counter systems
2-9.17 7 fev A. Sangnier Verification of programs with linked-lists and arrays
2-9.18 14 fev A. Sangnier Verification of concurrent programs
2-9.19 21 fev Sangnier Beyond reachability in counter systems
2-9.20 28 fev semaine de révision
2-9.20 6 mar Final examination


There will be an examination at mid-term and one at the end. Both examinations will be on the corresponding parts of the course only.

* Examinations 2010-11: mid-term of november 2010 including corrections, full-term (part 1) of february 2011

* Examinations 2009-10: mid-term of november 2009, full-term of february 2010

* Examinations 2008-09: mid-term of november 2008,full-term of february 2009.


Teachers for 2011—2012


Lecture notes

Lectures notes or slides will be put on-line as soon as possible after each course.


  • Model Checking. E.M. Clarke, O. Grumberg, D.A. Peled. MIT Press, 1999.
  • Systems and Software Verification. Model-Checking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Springer 2001.

Specific references

  • [Kru72]
    J. B. Kruskal.
    The theory of well-quasi-ordering: A frequently discovered concept.
    In Journal of Combinatorial Theory, Series A, 13(3):297—305, 1972.
  • [PR04]
    A. Podelski and A. Rybalchenko.
    Transition invariants.
    In Proc. LICS 2004, pp 32—41. IEEE Comp. Soc. Press 2004.

Previous years


A. Bouajjani PU Paris 7 LIAFA
A. Finkel PU ENS de Cachan LSV
P. Habermehl MC Paris 7 LIAFA
Y. Jurski MC Paris 7 LIAFA
A. Sangnier MC PARIS 7 LIAFA
Ph. Schnoebelen DR CNRS LSV
M. Sighireanu MC Paris 7 LIAFA

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