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 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. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Esparza, J., Kiefer, S., & Schwoon, S. (2006). Abstraction refinement with craig interpolation and symbolic pushdown systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3920 LNCS, pp. 489–503). https://doi.org/10.1007/11691372_35
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
