Static analysis of fault-tolerant distributed algorithms – SAFTA

Fault-tolerant distributed data structures are at the core distributed systems.
Due to the multiple sources of non-determinism, their development is challenging.
The project aims to increase the confidence we have in distributed implementations of data structures.
We think that the difficulty does not only come from the algorithms but from the way we think about distributed systems.
We will investigate partially synchronous programming abstractions that reduce the number of interleavings, simplifying the reasoning about distributed systems and their proof arguments.
We will use partial synchrony to define reduction theorems from asynchronous semantics to partially synchronous ones, enabling the transfer of proofs from the synchronous world to the asynchronous one.
Moreover, we will define a domain specific language, that allows the programmer to focus on the algorithm task, it compiles into efficient asynchronous code, and it is equipped with automated verification engines.