A New Refinement Strategy for CEGAR-Based Industrial Model Checking

Martin Leucker, Grigory Markin, Martin R. Neuhäußer


This paper presents a novel refinement strategy in the setting of counterexample-guided abstraction refinement (CEGAR)-based model checking. More specifically, the approach shown builds on lazy abstraction in the context of predicate abstraction. While the concept of interpolants is typically used for refinement, this paper employs unsatisfiability cores together with weakest preconditions. The new refinement technique is especially applicable in the setting where interpolants are hard to compute, such as for McCarthy’s theory of arrays or for the theory of fixed-width bit vectors. It is implemented within a model-checking tool developed for the verification of industrial-critical systems and outperforms current refinement strategies on several examples.

Original languageEnglish
Title of host publicationHardware and Software: Verification and Testing
Editors N. Piterman
Number of pages16
Place of PublicationCham
PublisherSpringer Verlag
Publication date28.11.2015
ISBN (Print)978-3-319-26286-4
ISBN (Electronic)978-3-319-26287-1
Publication statusPublished - 28.11.2015
Event11th International Haifa Verification Conference - Haifa, Israel
Duration: 17.11.201519.11.2015
Conference number: 154279


Dive into the research topics of 'A New Refinement Strategy for CEGAR-Based Industrial Model Checking'. Together they form a unique fingerprint.

Cite this