Distributed Algorithms: A Challenging Playground for Model Checking (Invited Talk)

Distributed computing is increasingly spreading, in advanced technological applications as well as in our daily life. Failures in distributed algorithms can have important human and financial consequences, so that is is crucial to develop rigorous techniques to verify their correctness. Model checking is a model-based approach to formal verification, dating back the 80’s. It has been successfully applied first to hardware, and later to software verification. Distributed computing raises new challenges for the model checking community, and calls for the development of new verification techniques and tools. In particular, the parameterized verification paradigm is nowadays blooming to help proving automatically the correctness of distributed algorithms. In this invited talk, we present recent parameterized verification developments to automatically prove properties of some classical distributed algorithms.