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

摘要: Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: they have multiple parameters that are restricted by arithmetic conditions, the number processes and faults parameterized, algorithm code parameterized due to conditions counting received messages. Recently, we introduced a technique first applies data counter abstraction then runs bounded model checking (BMC). Given an FTDA, our computes upper bound on diameter system. This makes BMC complete: it always finds counterexample, if there actual error. To verify state-of-the-art FTDAs, further improvement needed. In this paper, encode executions over integer counters in SMT. We introduce new form offline partial order reduction exploits acceleration structure FTDAs. aggressively prunes execution space be explored solver. way, verified safety seven FTDAs were out reach before. Open image window