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.

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

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.

Here are some new (for the year 2011-2012) research internships related to the topics of the course:

• ANR project ReacHard with Master and thesis proposals
• Robots games proposed by L. Doyen;
• Refined Karp and Miller tree proposed by A. Finkel and by J. Leroux;
• Post Embedding Problems, Dickson's Lemma, and Master Problems for Monotonic Counter Systems, proposed by S. Schmitz and by Ph. Schnoebelen;
• Semilinearity of Vector Addition Systems with States, proposed by J. Leroux and by G. Sutre;
• Mathematical Structures for Reachability Sets and Relations, proposed by G. Sutre and by J. Leroux ;

Here are research internships of year 2010-2011:

• A Theory of Quantitative Languages,proposed by L. Doyen;
• Automatic Synthesis of Assertions about Programs with Data Structures, proposed by A. Bouajjani and C. Enea;
• Verification of concurrent programs for relaxed memory models, proposed by A. Bouajjani and G. Parlato;
• Verifying concurrent dynamic data structures, proposed by A. Bouajjani and M. Emmi;
• Constructing optimally robust concurrent programs w.r.t. relaxed memory models and program transformations, proposed by A. Bouajjani and M. Sighireanu.
• Angluin-style learning of non-deterministic tree automata, proposed by P. Habermehl and B. Bollig

• Laurent Doyen (12,5h)
• Alain Finkel (12,5h)
• Peter Habermehl (12,5h)
• Arnaud Sangnier (12,5h)

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.

• [BBH*06]
  A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar.
  Programs with Lists are Counter Automata.
  In Proc. CAV 2006, LNCS 4144, pp 517—531. Springer 2006.

• [BFLS06]
  S. Bardin, A. Finkel, É. Lozes, and A. Sangnier.
  From Pointer Systems to Counter Systems Using Shape Analysis.
  In Proc. AVIS 2006, Vienna, Austria, Apr. 2006.

• [BHJS07]
  A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu.
  Rewriting Systems with Data: A Framework for Reasoning about Systems with Unbounded Structures over Infinite Data Domains. In Proc. FCT 2007, LNCS 4639, pp 1—22. Springer 2007.

• [BIL09]
  M. Bozga, R. Iosif and Y. Lakhnech. Flat Parametric Counter Automata. Fundamenta Informaticae 91(2) pp 275—303, 2009.

• [BW02]
  B. Boigelot, P. Wolper.
  Representing arithmetic constraints with finite automata: An overview. In Proc. ICLP 2002, LNCS 2401, pp 1—19. Springer 2002.

• [Coo72]
  D. C. Cooper.
  Theorem Proving in Arithmetic without Multiplication
  in Machine Intelligence 7, pp 91—99. 1972

• [DJS99]
  C. Dufourd, P. Jančar, and Ph. Schnoebelen.
  Boundedness of Reset P/T nets.
  In Proc. ICALP '99, LNCS 1644, pp 301—310. Springer 1999.

• [EFM99]
  J. Esparza, A. Finkel and R. Mayr.
  On the verification of broadcast protocols.
  In Proc. LICS 1999, pp 352—359. IEEE Comp. Soc. Press 1999.

• [Esp98]
  J. Esparza.
  Decidability and complexity of Petri net problems - an introduction.
  In Advances in Petri Nets 1998, LNCS 1491, pp 374—428. Springer 1998.

• [FL02]
  A. Finkel and J. Leroux.
  How to compose Presburger accelerations: Applications to broadcast protocols.
  In Proc. FSTTCS 2002, LNCS 2256, pp 145—156. Springer 2002.

• [FS01]
  A. Finkel and Ph. Schnoebelen.
  Well structured transition systems everywhere!
  Theoretical Computer Science, 256(1—2):63—92, 2001.

• [FS08]
  A. Finkel and A. Sangnier.
  Reversal-Bounded Counter Machines Revisited.
  In Proc. MFCS 2008, LNCS 5162, pp. 323—334. Springer 2008.

• [FR74]
  M.J. Fischer and M. O. Rabin
  Super-exponential complexity of Presburger arithmetic.
  Technical Report, MIT-LCS-TM-043, 1974.

• [Hab97]
  P. Habermehl.
  On the Complexity of the Linear-Time mu-calculus for Petri Nets
  In Proc. ICATPN'97, LNCS 1248, pp 102—116. Springer 1997.

• [HIV08]
  P. Habermehl, R. Iosif, and T. Vojnar.
  A Logic of Singly Indexed Arrays.
  In Proc. LPAR 2008, LNAI 5330, pp 558—573. Springer 2008.

• [HP79]
  J.E. Hopcroft, and J.-J. Pansiot.
  On the Reachability Problem for 5-Dimensional Vector Addition Systems.
  In Theoretical Computer Science, 8:135—159. 1979.

• [Iba78]
  O. Ibarra.
  Reversal-bounded multicounter machines and their decision problems.
  J. ACM, 25(1):116—133, 1978.

• [Jan95]
  P. Jančar.
  Undecidability of bisimilarity for Petri nets and some related problems.
  Theoretical Computer Science, 148(2):281—301, 1995.

• [JMK01]
  P. Jančar,
  A. Kučera, and R. Mayr.
  Deciding bisimulation-like equivalences with finite-state processes.
  Theoretical Computer Science, 258(1—2):71—99, 2001.

• [Kla04]
  F. Klaedtke.
  On the Automata Size for Presburger Arithmetic.
  In Proc. LICS 2004, pp 110—119. IEEE Comp. Soc. Press, 2004

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

• [LS05]
  J. Leroux and G. Sutre
  Flat counter automata almost everywhere!.
  In Proc. ATVA 2005, LNCS 3707, pp 489—503. Springer 2005.

• [May03]
  R. Mayr.
  Undecidable problems in unreliable computations.
  Theoretical Computer Science, 297(1—3):337—354, 2003.

• [PR04]
  A. Podelski and A. Rybalchenko.
  Transition invariants.
  In Proc. LICS 2004, pp 32—41. IEEE Comp. Soc. Press 2004.

• [Sch10]
  Ph. Schnoebelen.
  Lossy Counter Machines Decidability Cheat Sheet.
  In Proc. RP 2010, LNCS 6227, pp 51—75. Springer, 2010.

• [WB00]
  P. Wolper, B. Boigelot.
  On the Construction of Automata from Linear Arithmetic Constraints
  In Proc. TACAS 2000, LNCS 1785, pp 1—19. Springer 2000.