Igor Konnov

Date: 17:00, Thursday, April 16, 2015
Speaker: Igor Konnov
Venue: IST Austria

Automatic verification of threshold-based fault-tolerant distributed algorithms
(FTDA) is challenging: FTDAs have multiple parameters that are restricted by
arithmetic conditions, the number of processes and faults is parameterized, and
the algorithm code is parameterized due to conditions involving counting the
number of received messages. Recently, we introduced a technique that first
applies data and counter abstraction and then runs bounded model checking
(BMC).  Given an FTDA, our technique computes an upper bound on the diameter of
the system.  Thus, BMC is complete in the sense that it will always find a
(possibly spurious) counterexample in the case of an actual error.

While our technique was the first to scale to FTDAs from the classic
distributed computing literature, more improvement is needed to verify
state-of-the-art algorithms.  In this paper, we encode bounded executions over
integer counters in SMT.  By exploiting the structure of the FTDAs with a new
form of offline partial order reduction, we aggressively cut the execution
space that must be explored by the solver.  Our approach outperforms existing
methods by up to two orders of magnitude.  Thus, we verified safety of seven
FTDAs that were out of reach before.

Posted in RiSE Seminar