@inproceedings{c6f142e3aab2409f9b52b894fd40d237,
title = "Abstraction refinement with craig interpolation and symbolic pushdown systems",
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.",
author = "Javier Esparza and Stefan Kiefer and Stefan Schwoon",
year = "2006",
doi = "10.1007/11691372_35",
language = "English",
isbn = "3540330569",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "489--503",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 12th International Conference, TACAS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006",
note = "12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006 ; Conference date: 25-03-2006 Through 02-04-2006",
}