• 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.

En raison de la grève appelée par l’intersyndicale, la première séance prévue le 18 septembre est reportée au 25 septembre. François Laroussinie sera néanmoins présent entre 12h45 et 13h pour discuter avec les étudiant-e-s présent-e-s intéressé-e-s par le cours.

Due to the strike called by the inter-union, the first session scheduled for 18 September is postponed to 25 September. François Laroussinie will nevertheless be available from 12:45 to 13:00 to talk with any students interested in the course.

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

Runtime verification is a lightweight verification technique that, in contrast to most other techniques presented in the lecture, is independent of a model and, therefore, applicable to black-box systems that are not accessible as a whole. However, resorting to techniques from temporal logic, automata theory, and timed systems, we can construct devices that monitor system executions and raise the alarm once we can be sure a specification has been violated or satisfied. This part of the lecture focuses on various specification formalisms (including real-time-based languages such as MTL) and classifying properties into monitorable ones and those unsuitable for this kind of verification technique. The lecture will be based on scientific articles surveying existing literature and presenting original results:

• Volker Diekert, Martin Leucker: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537: 29-41 (2014)
• Andreas Bauer, Martin Leucker, Christian Schallhart: Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4): 14:1-14:64 (2011)
• Oded Maler, Dejan Nickovic: Monitoring Temporal Properties of Continuous Signals. FORMATS/FTRTFT 2004: 152-166