Reference: Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In Holger Hermanns and Jens Palsberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of Lecture Notes in Computer Science, pages 489–503, Vienna, Austria, 2006. 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. Suggested BibTeX entry: @inproceedings{EKS06b,     address = {Vienna, Austria},     author = {Javier Esparza and Stefan Kiefer and Stefan Schwoon},     booktitle = {Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},     editor = {Holger Hermanns and Jens Palsberg},     pages = {489--503},     series = {Lecture Notes in Computer Science},     title = {Abstraction Refinement with {Craig} Interpolation and Symbolic Pushdown Systems},     volume = {3920},     year = {2006} }

GZipped PostScript (182 kB) PDF (174 kB) Tech report version