**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.