SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms

POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms Igor Konnov, Helmut Veith, and Josef Widder TU Wien (Vienna University of Technology) Abstract. Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: they 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 counting the number of received messages. Recently, we ina 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. This makes BMC complete: it always finds a counterexample, if there is an actual error. To verify state-of-the-art FTDAs, further improvement is needed. In this paper, we encode bounded executions over integer counters in SMT. We introduce a new form of offline par...

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: Igor Konnov, Helmut Veith, Josef Widder
• Keywords: CAV 2015, Hardware