Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

[Home page]

[How to contact us]
[How to apply]
[Entrance requirements]
[Management]

[The MPRI course]

[Organisation]
[Standard courses]
[Level 1 modules]
[Level 2 modules]
[Teaching staff]

[Practical information]

[Calendar and timetable]
[Student directory]
[Examinations calendar]
[Internships]
[Scolarships]

Vérification de systèmes dynamiques et paramétrés (48h, 6 ECTS)

Responsables : Ahmed Bouajjani (LIAFA, Univ. Paris 7) et Philippe Schnoebelen (LSV, ENS de Cachan).

Le cours a lieu le vendredi de 12h45 à 15h45 à Chateau des Rentiers.

Table des matières

Motivations et objectifs du cours

Depuis 1990, les techniques algorithmiques de vérification des systèmes sont utilisées dans des secteurs de plus en large de l'industrie, et sont capables de prendre en compte des aspects de plus en plus variés des systèmes. Le cours 2-9 présente certaines avancées récentes dans le domaine de la vérification automatique par model-checking, spécialement en ce qui concerne la vérification de modèles avec un nombre infini de configurations, permettant d'analyser et de valider des systèmes dynamiques et paramétrés complexes tels que systèmes logiciels embarqués, algorithmes distribués, protocoles de télécommunication modernes, etc.

L'outil de base étudié dans ce cours est les systèmes à compteurs, qui représentent un modèle fondamental du point de vue théorique. Ainsi, le cours présente en passant quelques résultats classiques qui sont d'intérêt général pour le bagage d'un chercheur, au delà du thème de la vérification. Il s'agit, par exemple, de la logique de Presburger, du lien avec la notion d'ensemble semilinéaire, de l'indécidabilité pour les machines de Minsky, pour le 10e problème de Hilbert, etc.

Langues du cours

Le cours sera en français sauf si des étudiants non-francophones demandent à ce qu'il soit en anglais et si l'ensemble des étudiants donnent leur accord. Le sujet d'examen sera en français et en anglais si le cours est en anglais.

Prérequis & cours voisins

Suivre utilement le cours 2-9 suppose de posséder quelques notions de base en calculabilité et complexité, en logique, et de bien maîtriser les concepts à la base de la théorie des automates finis et des langages réguliers.

Le cours 2-9 s'inscrit tout naturellement dans la suite du cours 1-22 qui fait une introduction générale au domaine de la vérification. Toutefois, le cours 1-22 n'est pas un pré-réquis.

Le cours 2-8 sur la vérification des systèmes temporisés, hybrides ou concurrents est complémentaire. Il met en oeuvre une démarche similaire à la nôtre mais en mettant l'accent sur les aspects temporisés.

Plan du cours

Partie I : Systèmes à compteurs et beaux ordres

Cours	Date	Intervenant	Contenu	Biblio	Notes de cours
2-9.1	18 sep	A. Finkel	Les systèmes à compteurs: un modèle fondamental. Un exemple de vérification d'un programme impératif. Un exemple de modélisation et de vérification d'un protocole broadcast		exercice 1 de l'examen de février 2009, notes-2-9-1, exercice-2-9-1
2-9.2	25 sep	A. Finkel	Des familles de systèmes à compteurs: Relationnels, fonctionnels, affines, linéaires, translations, machines de Minsky, systèmes d'addition de vecteurs (VAS) et réseaux de Petri. Indécidabilité de la terminaison et de l'accessibilité d'une machine de Minsky, décidabilité pour les VAS.	cf. notes de cours	notes-2-9-2.pdf
2-9.3	2 oct	A. Finkel	Définition des well-quasi-orderings (aussi WQO ou beaux ordres). Lemme de Dickson et lemme de Higman. Systèmes de transitions bien structurés (WSTS). Exemples de VAS étendus bien structurés ou non. Décidabilité de la terminaison et de la finitude pour les systèmes bien structurés (WSTS).	FS01	notes-2-9-3
2-9.4	9 oct	A. Finkel	WSTS: Décidabilité des problèmes de sûreté, couverture, accessibilité d'un état de contrôle, inévitabilité. Décidabilité des propriétés de liveness pour les systèmes à compteurs très bien structurés (VAS).	FS01
2-9.5	16 oct	M. Sighireanu	Indécidabilité de la finitude et du model-checking pour les systèmes à compteurs bien structurés (VAS avec reset,...).	May03	notes-2-9-5
2-9.6	23 oct	M. Sighireanu	Ensembles clos par le haut. Structures de données: CST.	[cf. notes de cours]	notes-2-9-6

Partie II : Systèmes à compteurs et arithmétique de Presburger

Cours	Date	Intervenant	Contenu	Biblio	Notes de cours
2-9.7	30 oct	P. Habermehl	Arithmétique de Presburger. Décidabilité par la méthode d'élimination de quantificateurs.	Coo72	slides-2-9-7
2-9.8	6 nov	P. Habermehl	Décidabilité via les automates finis. Systèmes à compteurs avec ensemble d'accessibilité définissable dans l'arithmétique de Presburger.	Kla04 WB00	slides-2-9-8
2-9.9	27 nov	P. Habermehl	Extension aux nombres réels. Automates faibles de Büchi.	BW02	slides-2-9-9
2-9.10	4 déc	P. Habermehl	Borne inférieure de la complexité de l'arithmétique de Presburger. Ensemble Presburger définissable = ensemble semi-linéaire. Applications.		slides-2-9-10
2-9.11	11 dec	M. Sighireanu	Vérification des systèmes à compteurs plats par accélération de circuits. Décidabilité et indécidabilité. L'accélération d'une fonction Presburger-linéaire à monoïde fini et extension aux systèmes plats. Techniques d'aplatissement. L'outil FAST. Études de cas aplatissables.	BFLS05	notes-2-9-11
2-9.12	18 déc	M. Sighireanu	Clôtures transitives de relations définies par DBM.	BIL06	notes-2-9-12

Partie III : Modélisation et vérification de programmes

Cours	Date	Intervenant	Contenu	Biblio	Notes de cours
2-9.13	8 jan	A. Bouajjani	Terminaison des programmes: invariants de transition bien fondés.	PR04
2-9.14	15 jan	A. Bouajjani	Terminaison des programmes: synthèse de ranking functions.		transparents
2-9.15	22 jan
2-9.16	29 jan	A. Bouajjani	Vérification de programmes avec tableaux. Séance de révision.	BHJS07,HIV08

Examens

Le contrôle des connaissances se fera sous la forme d'un partiel et d'un examen. L'examen ne concernera que la deuxième partie du cours (du cours 2-9-9 au cours 2-9-16 inclus). L'examen aura lieu le 5 février à l'horaire et au lieu du cours.

Stages d'initiation à la recherche

Les enseignants du cours 2-9 proposent des stages de M2 :

Lossy Counter Machines, proposé par Ph. Schnoebelen, LSV, ENS Cachan.
Weak memory models, proposé par Ahmed Bouajjani, LIAFA, Univ. Paris Diderot.
Vérification de programmes avec mémoire dynamique, proposé par Mihaela Sighireanu et Ahmed Bouajjani, LIAFA, Univ. Paris Diderot.
Accelerated Paths in Petri Nets, proposé par Alain Finkel et Sylvain Schmitz, LSV, ENS Cachan.

Intervenants pour 2009—2010

Bibliographie

Supports de cours

Les notes de cours et les feuilles d'exercice seront mises en ligne immédiatement après chaque cours. Ces notes de cours seront suffisantes pour la comprehension du cours.

Généralités

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.

Références spécifiques

Nous listerons ici les articles auxquels font référence nos notes de cours.

[BW02] B. Boigelot, P. Wolper. Representing arithmetic constraints with finite automata: An overview. In Proc. 18th Int. Conf. Logic Programming (ICLP 2002), Copenhagen, Denmark, July-Aug. 2002, volume 2401 of Lecture Notes in Computer Science, pages 1—19. Springer, 2002.

[Coo72] D. C. Cooper. Theorem Proving in Arithmetic without Multiplication in Machine Intelligence. Edinburgh University Press: 91–100. 1972

[DJS99] C. Dufourd, P. Jancar, and Ph. Schnoebelen. Boundedness of Reset P/T nets. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP '99), pages 301—310, Prague, Czech Republic, July 1999.

[Esp98] J. Esparza. Decidability and complexity of Petri net problems - an introduction. In Advances in Petri Nets 1998, vol. 1491 of Lect. Notes Computer Science, pages 374—428, 1998.

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

[Hab97] P. Habermehl. On the Complexity of the Linear-Time mu-calculus for Petri Nets Proceedings of the 18th International Conference on Applications and Theory of Petri Nets (ICATPN'97), vol. 1248 of Lecture Notes in Computer Science, Springer-Verlag, pages 102—116

[HIV08] P. Habermehl, R. Iosif, and T. Vojnar. A Logic of Singly Indexed Arrays. In Proc. of 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning---LPAR'08, Doha, Qatar, volume 5330 of LNAI, pages 558--573, 2008. Springer-Verlag.

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

[Kla04] F. Klaedtke. On the Automata Size for Presburger Arithmetic. In the Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)., pages 110--119. IEEE Computer Society Press, 2004

[WB00] P. Wolper, B. Boigelot. On the Construction of Automata from Linear Arithmetic Constraints In Proc. Tools and Algorithms for the Construction and Analysis of Systems, volume 1785, Lecture Notes in Computer Science, pages 1-19, Berlin, March 2000, Springer-Verlag.

[AJ96a] P. A. Abdulla et B. Jonsson. Verifying programs with unreliable channels. Information & Computation, 127(2) pp 91-101, 1996.

[AJ96b] P. A. Abdulla et B. Jonsson. Undecidable verification problems for programs with unreliable channels. Information & Computation, 130(1) pp 71-90, 1996.

[BW02] B. Boigelot, P. Wolper. Representing arithmetic constraints with finite automata: An overview. In Proc. 18th Int. Conf. Logic Programming (ICLP 2002), Copenhagen, Denmark, July-Aug. 2002, volume 2401 of Lecture Notes in Computer Science, pages 1—19. Springer, 2002.

[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. LICS, IEEE 2004.

[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. 16th Intern. Symp. on Fundamentals of Computation Theory (FCT'07). LNCS 4639, Budapest (Hungary), August 2007.

[BIL06] M. Bozga, R. Iosif and Y. Lakhnech. Flat Parametric Counter Automata. ICALP'06, extended version in Fundamenta Informatica 91 (2), 275 - 303.

[BFLS05] S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat Acceleration in Symbolic Model Checking. In ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of LNCS, pages 474-488, 2005. Springer.

Les années précédentes

Annales 2008: partiel, examen.

Pages Web:

Équipe pédagogique

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
S. Kremer	CR	INRIA	LSV
Ph. Schnoebelen	DR	CNRS	LSV
M. Sighireanu	MC	Paris 7	LIAFA
T. Touili	CR	CNRS	LIAFA