[Back]

I. Konnov, M. Lazić, H. Veith, J. Widder:
"Parameterized Verification of Liveness of Distributed Algorithms";
Talk: Workshop on Formal Reasoning in Distributed Algorithms (FRiDA), Marrakech, Marocco; 2016-05-17.

The interplay of safety and liveness is essential for fault-tolerant distributed algorithms. Still, existing parameterized verification literature heavily focuses on safety properties, e.g., reachability. We introduce an automated method for parameterized model checking of liveness properties of distributed algorithms. Our method is based on a small counterexample property that states that, despite parameterization, counterexamples have a predictable size and structure. We substantiate our theoretical results by an experimental evaluation in which we verify liveness of state-of-the-art fault-tolerant distributed algorithms, most of which were out of reach for existing techniques.

model checking, fault tolerance, parameterized verification

Project Head Igor Konnov:
Abstraction-based Parameterized TLA Checker

Project Head Josef Widder:
Parametrized Verification of Fault-tolerant Distributed Algorithms