01.08.2012
Counterexample-guided abstraction refinement for symmetric concurrent programs
Erschienen in: Formal Methods in System Design | Ausgabe 1/2012
EinloggenAktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
C
code. In contrast, there is little evidence of fruitful applications of CEGAR 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 absorbed by exploiting symmetry. We have implemented our method in a tool, SymmPa, and demonstrate its superior performance over alternative approaches on a range of synchronisation programs.