
Verification of dynamic and parameterized systems (48h, 6 ECTS)
People in charge :
http://www.lsv.enscachan.fr/~finkel/Alain Finkel (LSV, ENS de Cachan), responsible for this year,
and,
http://www.liafa.jussieu.fr/~abou/ Ahmed Bouajjani (LIAFA, Univ. Paris 7)
and,
http://www.lsv.enscachan.fr/~phs/ Philippe Schnoebelen (LSV, ENS de Cachan).
The lectures take place on Tuesday from 16h15 until 18h45 at the Chevaleret building (room 1E01).
Contents
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 29 presents certain recent advances in the domain ofautomatic verification by modelchecking,
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.
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).
To follow the course 29 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 29 is a quite natural followup of the course 122 which is giving a general introduction
to the domain of verification. However, it is not necessary to have followed course 122.
The courses 26 (on abstract interpretation and application to verification and static analysis) , 28 (on the verification of timed, hybrid and concurrent systems:
it introduces a similar scientific approach but concentrates on timed aspects), 2361 about proof of programs, 272 about proofassistants and 2201 about games theory are all intetresting complements of course 29.
Course  Date  Teacher  Contents  References  Lecture notes and exercises 
29.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, ...  [EFM99]
A recent but uncomplete proof of the Syracuse problem  presentation course 29;
slides1stlecture;
Exercise: what are the reachable configurations for the 3 counter machine in the Feb. 2009 exam? 
29.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]  slides2ndlecture
Exercises lectures 1  2 to send before 26 september 
29.3  27 sep  A. Finkel  Definition of wellquasiorderings (also called WQO). Dickson's lemma and Higman's lemma. Wellstructured transition systems (WSTS). Examples of wellstructured (or not) extended VAS. Decidability of the termination and the finiteness problems of wellstructured transition systems(WSTS).Computability of predecessor sets Pre^*(X).  [FS01], [Kru72]  slides3rdlecture 
29.4  4 oct  A. Finkel  Monotonic (aka wellstructured) counter machines. Decidability of reachability & safety, termination. Computability of predecessor sets Pre^*(X). Undecidability of Büchi properties, of finiteness.   slides4thlecture
notesmonotonic CM;
Undecidability for reset 
29.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]
[FMP'04]  
Course  Date  Teacher  Contents  References  Lecture notes 
29.6  18 oct  Laurent Doyen  Reminder of twoplayer graph games with reachability and safety objectives. Monotonic games. General results of decidability and undecidability.  [ABO'03]  [1]
[2] 
29.7  25 oct  Laurent Doyen  Energy games. Definition, computational complexity, strategy complexity. Algorithm.  [BFLMS'08]
[BCDGR'11]  [3] 
29  1er nov  pas de cours    
29.8  8 nov  Laurent Doyen  Energy games with partial observation. Finite memory strategies. Decidability and undecidability results.  [DDGRT'10]  [4] 
29.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] 
29.10  22 nov  Laurent Doyen  Multicounter games. Generalized energy games. Strategy complexity and computational complexity.  [CDHR'10]
[BJK'10]
[KS'88]  [6] 
29  29 nov  Midterm exam    
Course  Date  Teacher  Contents  References  Lecture notes 
29.6  6 dec  P. Habermehl  Presburger arithmetic. Decidability by the quantifier elimination method.   Slides 
29.7  13 dec  P. Habermehl  Lowerbound for the complexity of Presburger arithmetic  [FR74]  Slides 
29.8  20 dec  Pas de cours    
29.8  3 jan  P. Habermehl  Decidability using finitestate automata.   Slides 
29.9  10 jan  P. Habermehl  Extension to real numbers using weak Büchi automata.   Slides 
29.10  17 jan  P. Habermehl  Presburger definable sets = semilinear sets. Applications.   Slides 
Course  Date  Teacher  Contents  Biblio  Lecture notes 
29.16  24 jan  A. Sangnier  Reachability in functional flat counter systems, flattable counter systems  [FL02] [LS05][HP79]  
29.17  31 jan  A. Sangnier  Reachability in relational flat counter systems   
29.17  7 fev  A. Sangnier  Verification of programs with linkedlists and arrays   
29.18  14 fev  A. Sangnier  Verification of concurrent programs   
29.19  21 fev  Sangnier  Beyond reachability in counter systems   
29.20  28 fev  semaine de révision    
29.20  6 mar  Final examination    
Here are some new (for the year 20112012) research internships related to the topics of the course:
Here are research internships of year 20102011:
Lectures notes or slides will be put online as soon as possible after each course.
Model Checking. E.M. Clarke, O. Grumberg, D.A. Peled. MIT Press, 1999.
Systems and Software Verification. ModelChecking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Springer 2001.
[Kru72]
J. B. Kruskal.
The theory of wellquasiordering: 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.
A. Bouajjani 
PU 
Paris 7 
LIAFA 
S. Demri 
DR 
CNRS 
LSV 
L. Doyen 
CR 
CNRS 
LSV 
A. Finkel 
PU 
ENS de Cachan 
LSV 
P. Habermehl 
MC 
Paris 7 
LIAFA 
Y. Jurski 
MC 
Paris 7 
LIAFA 
S. Kremer 
CR 
INRIA 
LSV 
A. Sangnier 
MC 
PARIS 7 
LIAFA 
Ph. Schnoebelen 
DR 
CNRS 
LSV 
M. Sighireanu 
MC 
Paris 7 
LIAFA 
T. Touili 
CR 
CNRS 
LIAFA 
