Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-2567
Authors: Esparza, Javier
Kiefer, Stefan
Schwoon, Stefan
Title: Abstraction refinement with craig interpolation and symbolic pushdown systems
Issue Date: 2006
metadata.ubs.publikation.typ: Arbeitspapier
Series/Report no.: Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik;2006,2
URI: http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-25211
http://elib.uni-stuttgart.de/handle/11682/2584
http://dx.doi.org/10.18419/opus-2567
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.
Appears in Collections:05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Files in This Item:
File Description SizeFormat 
TR_2006_02.pdf219,29 kBAdobe PDFView/Open


Items in OPUS are protected by copyright, with all rights reserved, unless otherwise indicated.