Parametric Verification of Dynamic Distributed Systems

PaVeDyS is funded by ANR under grant number ANR-23-CE48-0005. The project starts on January 16th 2024 for a duration of 4 years. A short presentation of the project goals and organisation is available.


  1. VERIMAG (Grenoble) : Radu Iosif (PI), Marius Bozga, Karine Altisen, Lucas Bueri
  2. LABRI (Bordeaux) : Igor Walukiewicz, Hugo Gimbert, Anca Muscholl, Mikhail Raskin, Corto Mascle
  3. INRIA (Rennes) : Nathalie Bertrand, Thierry Jeron, Nicolas Markey, Ocan Sankur, Nicolas Waldburger
  4. IRIF (Paris) : Marie Fortin, Ahmed Bouajjani, Lucie Guillou, Jeremy Ledent
  5. DIBRIS (Genova) : Arnaud Sangnier (external partner)


Applications of distributed systems are omnipresent. They allow sharing resources and data. They are used to coordinate activities across multiple nodes, as in geographically distributed systems. Furthermore, they increase the resilience of systems through fault tolerance, availability, and recovery mechanisms. Designing, understanding, and validating distributed systems is challenging because of the huge number of interactions between components, some potentially leading to unpredictable scenarios. Early detection of design errors is not only crucial for financial reasons, but it is often the only feasible way to find critical errors. The methods for ensuring the correctness of distributed systems are not yet mature. This is particularly the case for the mechanized reasoning methods that we propose to develop in this project.


  1. Kick-off meeting: IRIF, Paris, January 16 2024