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

Techniques avancées de vérification / Advanced Techniques of Verification (2023-2024)

  • The lecturers for 2023-2024 are Benedikt Bollig, Patricia Bouyer, and François Laroussinie
  • This course is 48h and corresponds to 6 ECTS.
  • Lectures will take place on Monday, 12:45-15:45, in Bat. Sophie Germain, Room 1004.
  • The first lecture takes place on September 18.
  • The first and the third parts of the course are given by default in French, but it can be decided that they will be in English. The second part is given in English. Exams can be taken in French or English.
  • The prerequisites are basic knowledge in automata theory, logics and complexity theory. It is advised to take or have taken course 1.22 “Introduction to verification”. Related courses include course 2.9.1 “Mathematical foundations of the theory of infinite transition systems” and 2.9.2 “Algorithmic verification of programs”, and 2.20.1 “Game-theoretic techniques in computer science” and 2.20.2 “Mathematical foundations of automata theory”.
  • The first exam (partiel) will take place on Monday, November 27, 12:45-15:45, in Bat. Sophie Germain, Room 1004.

Contents

The lecture covers advanced techniques for the verification of computing systems.

Outline of the course (2023-2024)

  1. Temporal logic for the specification of systems (François Laroussinie)
  2. Verification and artificial intelligence (Benedikt Bollig)
  3. Modeling and verification of timed and hybrid systems (Patricia Bouyer)

Part 1: Temporal logic for the specification of systems (François Laroussinie)

  1. Introduction of temporal logics (LTL, CTL,...)
  2. Automata technics for temporal logics:
    • alternating word-automata (defs, properties,...)
    • alternating tree-automata (defs, properties,...)
    • application to satisfiability and model-checking
  3. Complexity
  4. Expressivity
    • Distinguishing power
    • Expressive power

Part 2: Verification of Neural Networks (Benedikt Bollig)

Schedule

1st 30/10/2023 Basics of neural networks and the specification language NNL
2nd 06/11/2023 Decidability of NNL
3rd 04/12/2023 An efficiently solvable fragment of NNL
4th 18/12/2023 Recurrent neural networks
5th 08/01/2024 Attention and transformers

Lecture Notes

Lecture notes as of January 28, 2024.

Part 3: Modeling and verification of timed and hybrid systems (Patricia Bouyer)

The first lecture of this part will take place on January 22, 2024.

Timed automata have been designed in the early 1990's for representing discrete systems with real-time constraints. Verification algorithms have been developed for that model, and several software tools have been implemented and are used in practice. In this part of the lecture, we will learn basic of the verification of such systems, we will draw some limits for the automatic verification of timed systems, and, if time allows, we will present standard symbolic technics.

Lecture notes will be available after each lecture.

Date of exam: March 4. Notes de cours autorisées.

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA