• This course is 48h and corresponds to 6 ECTS.
• Lectures will take place on Thursday, 12:45-15:45, in Bat. Sophie Germain, Room 1004.
• The first lecture takes place on September 25, 2025.
• The course is given in French or English, depending on the audience. Exams can be taken in French or English.
• The prerequisites are background knowledge in areas like formal languages, automata theory, and logic.

The final exam will take place on Thursday, 12 March 2026, from 12:45 to 15:45 in Room 1004.

This course covers fundamental techniques to specify and verify systems, ensuring their correctness and robustness. It covers the theoretical foundations and practical applications of verification methods,

1. Temporal logic for the specification of systems (François Laroussinie)
2. Games for verification (Dietmar Berwanger)
3. Modeling and verification of timed and hybrid systems (Patricia Bouyer)
4. Runtime verification (Benedikt Bollig)

Temporal logics are a widely used formalism for specifying and verifying computer systems. There are many different temporal logics depending on the time model considered, the type of properties we want to express, etc. We will focus on two well-known logics: LTL (Linear-time Temporal Logic) and CTL (Computation Tree Logic). We will study the decision procedures for the satisfiability and model-checking and we will also consider the expressive power of these logics. Several extensions of these logics will be presented. We will use automata theory to solve all these questions: word automata for LTL and tree automata for CTL (no special prerequisite is assumed on this). Lecture notes will be provided. These results are classical and can be found in many papers, for example in:

• Automata: From Logics to Algorithms, Moshe Y. Vardi, Thomas Wilke, Logic and Automata 2008

This submodule delves into the game-theoretic modeling of reactive processes, i.e., processes that interact continually with their environment. The interaction can be seen as an infinite game between two players: one representing the process and the other the nondeterministic environment. The key question is whether the process player has a strategy to enforce a given specification or if the environment can invalidate it. We introduce the basic framework of infinite games on finite graphs with winning conditions that capture hard functional requirements such as safety, reachability, LTL, or omega-regular specifications. Further, we present extensions to softer requirements on resource optimisation given by quantitative conditions such as mean-payoff, energy or probabilistic objectives. Beyond immediate applications to model-checking and synthesis of reactive systems, the framework sets the foundations for various game-based methods in automata theory, logic, and graph structure theory.

• K. Apt and E. Grädel, Lectures in Game Theory for Computer Scientists, Cambridge University Press 2011
• E. Grädel, T. Wilke, W. Thomas, Automata, Logics, and Infinite Games, Lecture Notes in Computer Science vol. 2500, Springer 2002

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 submodule, we will learn the bases of the verification of such systems, and in particular the fundamental construction of the region automaton. We will also draw some limits for the automatic verification of timed systems, and will make an incursion in the world of hybrid systems. Lecture notes have been built over the years, and give many pointers to the literature. The complete lecture notes are available here (not everything will be taught in the course):

Lecture Notes (updated – there is a bit more than what we did during the course)

Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model. It is particularly useful for partially observable or black-box systems, where uncertainty can only be resolved through observation. Using temporal logic, automata theory, and epistemic reasoning, we study how monitors can infer whether a specification has been violated or satisfied from the information available so far. The lecture covers specification formalisms, diagnosis, opacity, and monitorability, and explains how offline analysis is used to construct monitors that operate online on observed executions.

Lecture Notes (in progress, updated after each lecture)