ANR project FREDDA

FoRmal mEthods for the Design of Distributed Algorithms

Distributed algorithms are nowadays omnipresent in most systems and applications. It is of utmost impor- tance to develop algorithmic solutions that are both robust and flexible, to be used in large scale applications. Currently, distributed algorithms are developed under precise assumptions on their execution context: syn- chronicity, bounds on the number of failures, etc. The robustness of distributed algorithms is a challenging problem which has barely been considered until now, and there is no systematic way to guarantee or verify the behavior of an algorithm beyond the context for which it has been designed. We propose to develop automated formal method techniques to verify the robustness of distributed algorithms and to support the development of robust applications. Our methods are of two kinds: statically through classical verification, and dynamically, by synthesizing distributed monitors, that check either correctness or the validity of the context hypotheses at runtime.

The proposal of the project FREDDA can be found here.