Form Methods Syst Des (2012) 41:25–44 DOI 10.1007/s10703-012-0155-3 Counterexample-guided abstraction refinement for symmetric concurrent programs

Abstract Predicate abstraction and counterexample-guided abstraction refinement (CE-GAR) have enabled finite-state model checking of software written in mainstream program-ming languages. This combination of techniques has been successful in analysing system-level sequential C code. In contrast, there is little evidence of fruitful applications of CE-GAR to shared-variable concurrent software. We attribute this gap to the lack of abstraction strategies that permit a scalable analysis of the resulting multi-threaded Boolean programs. The goal of this paper is to close this gap. We have developed a symmetry-aware CEGAR technique: it takes into account the replicated structure of programs that consist of many threads executing the same procedure, and generates a Boolean program template whose multi-threaded execution soundly overapproximates the original concurrent program. State explosion during model checking parallel instantiations of this template can now be ab-sorbed by exploiting symmetry. We have implemented our method in a tool, SYMMPA, an