Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-2567
Full metadata record
DC FieldValueLanguage
dc.contributor.authorEsparza, Javierde
dc.contributor.authorKiefer, Stefande
dc.contributor.authorSchwoon, Stefande
dc.date.accessioned2006-01-25de
dc.date.accessioned2016-03-31T07:58:33Z-
dc.date.available2006-01-25de
dc.date.available2016-03-31T07:58:33Z-
dc.date.issued2006de
dc.identifier.other260384798de
dc.identifier.urihttp://nbn-resolving.de/urn:nbn:de:bsz:93-opus-25211de
dc.identifier.urihttp://elib.uni-stuttgart.de/handle/11682/2584-
dc.identifier.urihttp://dx.doi.org/10.18419/opus-2567-
dc.description.abstractCounterexample-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.en
dc.language.isoende
dc.relation.ispartofseriesTechnischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik;2006,2de
dc.rightsinfo:eu-repo/semantics/openAccessde
dc.subject.classificationModel checkingde
dc.subject.ddc004de
dc.subject.otherCEGARde
dc.titleAbstraction refinement with craig interpolation and symbolic pushdown systemsen
dc.typeworkingPaperde
dc.date.updated2013-07-08de
ubs.fakultaetFakultät Informatik, Elektrotechnik und Informationstechnikde
ubs.institutInstitut für Formale Methoden der Informatikde
ubs.opusid2521de
ubs.publikation.typArbeitspapierde
ubs.schriftenreihe.nameTechnischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnikde
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.