Université Paris 7 École Normale Supérieure de Cachan École Normale Supérieure École Polytechnique
Université Paris 6 Université Paris 11 École Nationale Supérieure des Télécommunications
Centre National de la Recherche Scientifique Commissariat à l'Energie Atomique Institut National de Recherche en Informatique et en Automatique

Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

[Home page] [The MPRI course] [Practical information]


Foundations of quantitative and real-time verification (48h, 6 ECTS)

Fondements pour la vérification quantitative et temps-réel

Persons in charge: Paul Gastin (LSV, ENS Cachan) and François Laroussinie (LIAFA, Univ. Paris 7).

Year 2010-2011: Lecturers

Benedikt Bollig, Nicoals Markey, Marc Zeitoun.

Schedule:

To be announced.

Language:

To be decided with the students.

Students will be allowed to take the exam in French and in English.

Prerequisites and related courses:

Basic knowledge in automata theory, logics and complexity theory will be useful. It is advised to take or have taken course 1.22 "Introduction to verification".

Related courses include course 2.09 "Verification of dynamic and parameterized systems", and 2.20.1 "Game-theoretic techniques in computer science" and 2.20.2 "Mathematical foundations of automata theory".

Motivations and objectives of this course

Embedded systems are more and more widespread (in various applications including telecommunications, transportation, etc.), more and more complex, and often play a critical role. Verifying that they have the expected behaviour is often crucial, and formal verification of embedded systems (in particular model-checking) has been a very active field of research in the last 30 years.

This course focuses on quantitative aspects of model-checking, especially in the model of timed automata and several extensions.

Outline of the course

  1. Timed and hybrid automata [24h] (Nicolas Markey)
  2. Weighted automata [12h] (Marc Zeitoun)
  3. Modeling and verification of real-time distributed systems [12h] (Benedikt Bollig)

Detailled descrition

Part I: Timed and hybrid automata

Lecturer: Nicolas Markey.

This first part will span the first half of the course (8 lectures). The schedule below is tentative:

Sessions 9 and 10 will be revision courses for preparing the mid-term exam.

I will try to post lecture notes here after each course.

Part II: Weighted automata

Lecturer: Marc Zeitoun.

Tentative topics:

References for Part II:

Part III: Modeling and verification of real-time distributed systems

Lecturer: Benedikt Bollig.

Tentative topics:

References for Part III:

References

Previous courses

Staff

E. Asarin PU Paris 7 LIAFA
B. Bollig CR ENS Cachan LSV
P. Bouyer CR ENS Cachan LSV
S. Demri CR ENS Cachan LSV
P. Gastin PU ENS Cachan LSV
S. Haddad PU ENS Cachan LSV
F. Laroussinie PU Paris 7 LIAFA
N. Markey CR ENS Cachan LSV
A. Petit PU ENS Cachan LSV
M. Zeitoun PU Bordeaux LABRI & LSV