Cutoff Bounds for Consensus Algorithms

Thu 17Nov2016

Ognjen Maric, ETH Zurich

From 12.00 until 13.30

At ETH Zurich, CNB/F/110

Universitätstrasse 6, 8092 Zurich


Consensus algorithms are fundamental building blocks for fault-tolerant distributed systems and their correctness is critical. However, there are currently no fully-automated methods for their verification. The main difficulty is that the algorithms are parameterized: they should work for any given number of processes. We provide an expressive language for consensus algorithms and give cutoff bounds for it. Our cutoff bounds reduce parameterized verification to verifying consensus for finitely many processes. This is the first such result for fault-tolerant distributed systems. Our case studies yield bounds of 5 or 7, enabling practical verification using model checking.

Download Event to Calendar