Date: January 16th 2024, IRIF, Paris

Location: Sophie Germain Building (room 3058)

Programme

9h30-10h00 Welcome

10h00-10h50 Igor Walukiewicz (LABRI) : Characterizing consensus in the Heard-Of model

The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm. Joint work with A. R. Balasubramanian

11h00-11h50 Nathalie Bertrand (INRIA) : Verification of Randomized Consensus Algorithms with Probabilistic Threshold Automata*

Randomisation is a powerful tool to solve computationally hard problems: in distributed computing, probabilities can even permit to solve problems that are otherwise unsolvable, such as the consensus problem for asynchronous message- passing systems. Threshold automata were introduced by Konnov et al. to automatically prove safety and liveness properties in fault-tolerant non- probabilistic distributed algorithms. They fall short at representing randomized behaviours and algorithms working in rounds. We introduced a probabilistic variant of threshold automata, and designed model-checking algorithms to automatically verify whether given properties hold almost-surely (i.e. with probability 1). These are first steps towards the automated verification of randomised distributed algorithms. Joint work with Igor Konnov, Marijana Lazić and Josef Widder.

12h00-13h50 Lunch

14h00-14h30 Nicolas Waldburger (INRIA) : Parameterized Broadcast Networks with Registers

We consider the parameterized verification of networks of agents which communicate through unreliable broadcasts. In this model, agents have local registers whose values are unordered and initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test it for equality against one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable, although non-primitive recursive. We contrast this with the undecidability of the closely related target problem where all agents must synchronize on a given state. On the other hand, we show that the coverability problem is NP-complete when each agent only has one register.

14h30-15h00 Michael Raskin (LABRI) : Getting readable proofs for replicated systems from automated provers

The most powerful general systems for automatic search of rigorous proofs are probably First-Order Automated Theorem Provers. In this talk I will give an overview of a few papers (joint work with Christoph Welzel and Javier Esparza) where we have used FO ATPs for verification of parametric systems. The core of the approach is guessing which form of general invariants can be useful, then trying to prove such generalisations for finite-instance invariants.

15h00-15h30 Lucie Guillou (IRIF) : Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous

We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. We study the parameterised coverability problem of a configuration in this context, which consists in determining whether there is an initial number of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics. This is a joint work with Arnaud Sangnier and Nathalie Sznajder.

15h30-16h00 Coffee break

16h00-16h50 Radu Iosif (VERIMAG) : Self-Adapting Networks

We introduce a simple formal model to reason about the behaviors of self-adapting (reconfigurable) networks. The proofs of correctness of reconfiguration programs are done using a separation logic and a Hoare-style local reasoning proof system that produces proof obligations in the form of logical entailments. In particular, entailments are used to reason about invariance of assertions under interaction events (synchronous communication). In the second part of the talk, I will present some advances in deciding the validity of entailments in the dialect of separation logic used to model distributed networks. The decision procedure for the entailment problem relies on Courcelle’s Theorem stating the decidability of MSO for graphs of bounded tree-width and uses two novel techniques: 1. a computation of a bound on the tree-width of the models of a given separation logic formula (iff one exists) and 2. a push-button translation of (a significant fragment of) separation logic into MSO.

16h50-17h30 (the latest) Closing discussions