Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems

Javier Esparza, Stefan Kiefer, Stefan Schwoon

Abstract


Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as Binary Decision Diagrams (BDDs). We examine how Craig interpolants can be computed efficiently in this case and propose a new special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model checker Moped and report on experiments.

Keywords


model-checking, abstraction refinement, Craig interpolation, BDDs, push-down systems

Full Text:

PDF

Refbacks

  • There are currently no refbacks.