Tutorials
Sandrine Blazy
Université de Rennes, France
From mechanized semantics to verified compilation
Deductive verification provides very strong guarantees that software is bug-free. Since the verification is usually done at the source level, the compiler becomes a weak link in the production of software. Verifying the compiler itself provides guarantees that no errors are introduced during compilation.
This course will first introduce verified compilation and its associated semantic reasoning. Then, it will present CompCert, a fully verified compiler for C (using the Coq proof assistant) that is actually usable on real source code and that produces decent target code on real-world architectures. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software.
Pierre Ganty
IMDEA Software Institute, Madrid, Spain
A Uniform Framework for Language Inclusion Problems
We present a uniform approach for solving language inclusion problems.
Our approach relies on a least fixpoint characterization and a quasiorder to compare words of the “smaller” language, reducing the inclusion check to a finite number of membership queries in the “larger” language.
We present our approach in detail on the case of inclusion of a context-free language given by a grammar into a regular language.
We then explore other inclusion problems and discuss how to apply our approach.
Hugo Gimbert
CNRS, LaBRI, Univ. Bordeaux, France
Asynchronous distributed games
In an asynchronous distributed game, a team of players confronts the environment via an automaton. Team players must synchronize through shared actions, and can only communicate during these synchronizations. This talk will present several decidability and undecidability results for the problem of synthesizing winning strategies.
Nils Jansen
Ruhr-University Bochum, Germany
Decision-Making Under Uncertainty Meets Neurosymbolic AI – Foundations, Challenges, and Highlights
In this tutorial, we lay out the foundations of decision-making under uncertainty. We discuss standard models like Markov decision processes (MDPs) and the standard methods to solve these models. We then introduce their extensions to cope with various aspects of uncertainty, yielding models such as partially observable MDPs (POMDPs) or robust (PO)MDPs. We discuss how particular assumptions and solution methods made about standard MDPs are not possible anymore, as well as complexity aspects. In several research highlights, we introduce methods that fall in the realm of neurosymbolic artificial intelligence. In particular, we take the stance that besides classical AI planning approaches, a myriad of techniques from the area of formal verification are symbolic AI. These symbolic methods are augmented and complimented by modern deep reinforcement learning techniques.
Ocan Sankur
CNRS, IRISA, Univ. Rennes, France
Algorithms for Model Checking Timed Automata
Timed automata are a formalism that allows one to describe systems with discrete events and explicit time delays, and are expressive enough to capture the behaviors of real-time systems.
In this talk, I will present model checking algorithms for timed automata. The first part will focus on algorithms based on enumerative algorithms using zones, a special form of polyhedra used to represent clock values.
The second part focuses on other algorithms based on predicate abstraction, binary decision diagrams, and SMT solvers.
Jeremy Sproston
University of Turin, Italy
Model checking for probabilistic systems
When undertaking formal modelling and verification in many application contexts, including network protocols, robot navigation and systems biology, it is often important to represent and reason about the probability of system behaviours. This has led to the development of model-checking methods for such probabilistic systems and their implementation in model-checking tools.
In this tutorial, we will consider the basics of probabilistic model checking, focusing on the following topics: formalisms for the modelling of probabilistic systems, in particular discrete-time Markov chains and Markov decision processes; extensions of classical temporal logics for the specification of properties of probabilistic systems (such as PCTL); model-checking algorithms for discrete-time Markov chains and Markov decision processes.
Finally, we will also consider a number of ways in which the basic probabilistic model-checking approaches have been extended, considering in particular extensions for verifying system models that incorporate not only probabilities but also timing information.
Technical presentations
Matthias Függer
CNRS, LMF, University Paris-Saclay, France
Distributed Computing x Cells
We explore microbial cells as a material for computation. Due to pronounced stochastic effects we follow a distributed computational approach. This talk is about ongoing research and next steps.
Bas Luttik
Eindhoven U. of Technology, The Netherlands
Model checking shared-memory mutual exclusion algorithms
We will consider the verification, by model checking, of mutual exclusion algorithms that use shared memory for communication between threads. We focus on the following two questions:
(1) How to verify the mutual exclusion exclusion safety property without assuming that interactions with the shared memory are atomic?
(2) How to verify the starvation freedom liveness property when the model admits unrealistic computations that need to be excluded from consideration?
Jan Strejček
Masaryk University, Brno, Czech Republic
BDDs and their application in SMT solving
The talk will present the datastructure called Binary Decision Diagram (BDD) with its advantages and drawbacks. Then we provide the basics of the bitvector theory and explain its importance in the context of software verification. Further, we describe how BDDs can be used for SMT solving of the bitvector theory. After the naïve algorithm, we also introduce some methods and tricks that make the BDD-based approach to SMT solving competitive to state-of-the-art tools.
