Lectures

Schedule

The titles appearing in the schedule are abbreviated, the full titles and abstracts are given below.

Coffee breaks will take place at around 10:30 in the morning and 16:00 in the afternoon.

Student sessions will be organized on Monday, Tuesday, and Thursday at 16:30. They allow participants to present their ongoing work and receive feedback from the lecturers and other participants.

	Monday	Tuesday	Wednesday	Thursday	Friday
9:30-13:00	Jean-François Raskin	Davide Sangiorgi	Philipp Rümmer	Étienne André	Joël Ouaknine
	Reactive Synthesis	Coinduction	SMT & Interpolation	Timed Model Checking	p-adic Techniques
13:00-14:30	lunch	lunch	lunch	lunch	lunch
14:30-18:00	Romain Péchoux	Caterina Urban	Véronique Cortier	Timothy Bourke	Benoît Barbot
	Quantum Programs	Machine Learning	Electronic Voting	Scheduling Dataflow Programs	Probabilistic Systems
	Student session: Kinská, Lapointe, Villani, Dépernet	Student session: Mukhopadhyay, Ta, Möller, Marques		Student session: Herrmann, Andersen, Bonin, Renault
19:30			School dinner, Guinguette Pub Mac Carthy, Place Carnot

Tutorials (3 hours)

Étienne André, Nantes Université & LS2N, France

Timed Model Checking [part 1 | part 2]

The correctness of real-time systems, that mix concurrency with hard timing constraints, is important, yet challenging to achieve. Formal verification techniques such as model checking provide guarantees of correctness. This lecture will first focus on finite-state automata and temporal logics. Then we will focus on timed automata, an extension of finite-state automata with clocks measuring the elapsing of time, and on (timed) temporal logics. The course may also briefly mention parametric timed formalisms, turning very useful when the system is not known with full precision, or at early design stages.

Véronique Cortier, CNRS & LORIA, Nancy, France

Formal Verification of Electronic Voting Systems [slides]

Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages. We will see how to design secure electronic voting protocols and how to analyze them using formal methods, in order to detect attacks at an early stage, or prove security. In particular, we will see how to model and analyze voting protocols with ProVerif, a state-of-the-art tool for the analysis of security protocols.

Joël Ouaknine, Max Planck Institute for Software Systems, Saarbrücken, Germany

p-adic Techniques, with Applications to the Skolem Problem [part 1 | part 2]

I will present a gentle introduction to elementary p-adic techniques, with applications to the Skolem Problem, i.e., the question of determining, given a linear recurrence sequence over the integers (such as the Fibonacci numbers), whether the sequence has a zero. No prior exposure to p-adic techniques will be assumed.

Jean-François Raskin, Université Libre de Bruxelles, Belgium

Games and Learning for Reactive Synthesis [slides]

In this talk, we will review basic concepts in graph games and learning. We will then present recent contributions to the reactive synthesis problem that combine reactive synthesis with learning techniques.

Philipp Rümmer, University of Regensburg, Germany

Satisfiability and Craig Interpolation Modulo Theories (a Tutorial) [slides]

Satisfiability Modulo Theories (SMT) solvers are theorem provers used for various reasoning tasks in program verification: for checking the feasibility of execution paths, computing test inputs, verifying the correctness of loop invariants or function contracts, or inferring finite-state abstractions. The first part of this tutorial provides an introduction to the theory and practice of SMT solving, covering the architecture implemented by solvers, some of the main theories provided by solvers, as well as the interface used to integrate SMT solvers into verification systems. The second part of the tutorial focuses on Craig interpolation, a method for computing separating formulas for unsatisfiable conjunctions (or equivalently valid implications) that is a standard technique for constructing abstractions in model checking.

The second half of the tutorial is based on the recently completed handbook Theory and Applications of Craig Interpolation.

Davide Sangiorgi, University of Bologna, Italy

An Introduction to Coinduction and the Duality with Induction [slides available here]

Induction is a pervasive tool in Computer Science and Mathematics for defining objects and for proving properties on them. Coinduction is the dual of induction, and allows one to reason on objects that need not be hierarchically, or hereditarily, constructed. Today coinduction is widely used in Computer Science, but also in other fields, including Artificial Intelligence, Cognitive Science, Mathematics, Modal Logics, Philosophy.

In the talk I will review the basics of coinduction, with an emphasis on the difference and the duality with induction. I will also discuss bisimulation, one of the best known instances of coinduction, mainly employed to prove equalities among potentially infinite objects: processes or software applications that may continuously interact with their environment, streams, non-well-founded sets, and so on.

Technical presentations (1:30 hours)

Benoît Barbot, Université Paris-Est Créteil & LACL, France

Quantitative Model Checking of Probabilistic Systems [slides]

Qualitative model checking is often insufficient for analyzing probabilistic systems. In this talk, we will focus instead on quantitative questions, such as: “What is the probability of observing a failure in a large, redundant system?” We will explore the two main families of algorithms used to address these questions: numerical model checking and statistical model checking.

Additionally, we will examine tools that implement these algorithms.

Timothy Bourke, Inria, ENS Paris, France

Scheduling Multi-Rate Dataflow Programs with Constraint Solvers [slides]

Control software is often developed as a composition of step functions that execute cyclically and communicate via shared memory. Such software may be implemented manually in imperative languages like C or C++, with the individual functions being scheduled dynamically by a real-time kernel or statically by simply calling them in the required order. An alternative is to specify the control laws as functional “block diagrams”, in languages like Lustre and Scade 6, and to compile them to sequential code that executes in bounded time and memory. For safety-critical systems, this approach can help meet stringent traceability requirements, since it is easier to relate the source language to the system requirements.

Over the last few years, we’ve been working with Airbus to formalize and extend an approach for specifying and implementing control software with thousands of individual functions. The source language is an extension of Lustre where each function is associated with an execution rate specified as a fraction of the overall system period. Its semantics is given by a simple set of rules over infinite sequences. The language provides features for expressing constraints on resources and end-to-end latencies. These constraints, together with dataflow dependencies, are transformed into an Integer Linear Programming problem for treatment by solvers like IBM’s Cplex or Google’s CP-SAT. A solution assigns a phase to each function, which the compiler uses to produce a sequential executable.

This talk will present the basic ideas of dataflow synchronous languages and describe how we adapted them for specifying large multi-rate control software. We will describe the use of a constraint solver and the encoding of dependencies, resource constraints, and end-to-end latencies.

Romain Péchoux, Université de Lorraine & LORIA, Nancy, France

Towards the Verification of Quantum Programs [slides]

In this talk, we will provide a non-exhaustive overview of the problems involved and methods used to verify the properties of the quantum paradigm. We will begin by looking at the correctness properties of low-level models such as quantum circuits. We will then study quantum programs for which verification is crucial to guarantee properties such as physicality, feasibility, or termination.

Caterina Urban, Inria, ENS Paris, France

Abstract Interpretation-Based Static Analysis for Machine Learning Verification and Explainability [slides | tool]

Static analysis provides rigorous, automated techniques to reason about the behavior of software systems without executing them. Its use is well-established in industry to certify the safety and reliability of critical applications subject to stringent assurance and certification requirements.

With the rising prominence of machine learning, the integration of machine-learned components into critical systems presents novel challenges for static analysis techniques.

This lecture introduces static analysis in the context of machine learning software, with a particular focus on abstract interpretation–based methods. We survey existing approaches and discuss both their strengths and limitations through the dual lenses of verification and explainability, two key objectives for trustworthy machine learning systems.