Verification of Infinite State Systems Day @ IRIF
and Arnaud Sangnier HDR defense
WHEN & WHERE
Thursday 15th December 2022
Amphithéatre Pierre-Gilles de Gennes Bâtiment Condorcet
4 rue Alice Domont et Léonie Duquet 75013 Paris
PROGRAM
10:00 - Nathalie Bertrand - A CEGAR approach to parameterized verification of distributed algorithms
Abstract: Distributed algorithms are central to many domains such as scientific computing,
telecommunications and the blockchain. Even when they aim at performing simple
tasks, their behaviour is hard to analyze, due to the presence of faults
(crashes, message losses, etc.) and to the asynchrony between the processes.
Parameterized verification techniques have been developed to prove correctness
of distributed algorithms independently of actual setup, i.e. the number of
processes and the potential failures.
In this talk, we present a CEGAR approach to checking safety and liveness
properties for fault tolerant distributed algorithms that use threshold
conditions, typically on the number of received messages of a given type.
This is based on joint work with Bastien Thomas and Josef Widder.
11:00 - Jérôme Leroux - State Complexity of Protocols with Leaders
Abstract:Population protocols are a model of computation in which an arbitrary number of anonymous finite-memory agents are interacting in order to decide by stable consensus a predicate. In this presentation, we focus on the counting predicates that asks, given an initial configuration, whether the number of agents in some initial state i is at least n. In 2018, Blondin, Esparza, and Jaax shown that with a fix number of leaders, there exists infinitely many n for which the counting predicate is stably computable by a protocol with at most O(log log(n)) states. We provide in this presentation a matching lower-bound (up to a square root) that improves the inverse-Ackermannian lower-bound presented at PODC in 2021.
14:00 - Arnaud Sangnier- Algorithmic techniques for the verification of
counter systems and parameterised networks
- HDR defense
Abstract: Model-checking is a verification technique which is in the past has been successfully applied to verify automatically the behavior of finite state systems. This approach consists in modelling a computing system by a mathematical model, in translating its specification into a logical formalism and then in proposing algorithms to check whether a model satisfies a logical formula. When the considered models have an infinite number of states, this method can easily lead to undecidable model-checking problems and one has hence to find the right trade-off between the expressiveness of models and specification languages and the feasibility of the verification. In this thesis, I present my contributions to the field of verification of infinite states systems where I have considered two main families of models. The first one are counter systems which can be seen as programs manipulating variables (called counters) taking their value in the natural. The second one are parameterised networks which can be seen as an abstraction of distributed networks where the number of participating entities is not fixed a priori and is unbounded. For these different models, I study exhaustively when the automatic verification is feasible and in the positive cases I try to design model-checking algorithms with optimal complexity bounds.