Distributed and predictable software model checking
Nuno P. Lopes, Andrey Rybalchenko · 2011
Abstract. We present a predicate abstraction and refinement-based al-gorithm for software verification that is designed for the distributed ex-ecution on compute nodes that communicate via message passing, as found in today’s compute clusters. A successful adaptation of predi-cate abstraction and refinement from sequential to distributed setting needs to address challenges imposed by the inherent non-determinism present in distributed computing environments. In fact, our experiments show that up to an order of magnitude variation of the running time is common when a naive distribution scheme is applied, often resulting in significantly worse running time than the non-distributed version. We present an algorithm that overcomes this pitfall by making determin-istic the counterexample selection in spite of the distribution, and still efficiently exploits distributed computational resources. We demonstrate that our distributed software verification algorithm is practical by an experimental evaluation on a set of difficult benchmark problems from the transportation domain. 1