Table of Contents
## Techniques avancées de vérification / Advanced Techniques of Verification (2023-2024)- 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.
## ContentsThe lecture covers advanced techniques for the verification of computing systems. ## Outline of the course (2023-2024)- Temporal logic for the specification of systems (François Laroussinie)
- Verification and artificial intelligence (Benedikt Bollig)
- Modeling and verification of timed and hybrid systems (Patricia Bouyer)
## Part 1: Temporal logic for the specification of systems (François Laroussinie)- Introduction of temporal logics (LTL, CTL,...)
- Automata technics for temporal logics:
- alternating word-automata (defs, properties,...)
- alternating tree-automata (defs, properties,...)
- application to satisfiability and model-checking
- Complexity
- Expressivity
- Distinguishing power
- Expressive power
## Part 2: Verification of Neural Networks (Benedikt Bollig)## Schedule
## Lecture NotesLecture 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 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. - Lecture 1 on Jan 22, 2024
- Lecture 2 on Jan 29, 2024
- Lecture 3 on Feb 5, 2024
- Lecture 4 on Feb 12, 2024
- Lecture 5 on Feb 19, 2024
Date of exam: March 4. Notes de cours autorisées. |