Ognjen Maric, ETH Zurich
From 12.00 until 13.30
At ETH Zurich, CNB/F/110
Universitätstrasse 6, 8092 Zurich
Abstract
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.