Abstraction refinement with craig interpolation and symbolic pushdown systems

Esparza, Javier; Kiefer, Stefan; Schwoon, Stefan

Abstraction refinement with craig interpolation and symbolic pushdown systems

dc.contributor.author	Esparza, Javier	de
dc.contributor.author	Kiefer, Stefan	de
dc.contributor.author	Schwoon, Stefan	de
dc.date.accessioned	2006-01-25	de
dc.date.accessioned	2016-03-31T07:58:33Z
dc.date.available	2006-01-25	de
dc.date.available	2016-03-31T07:58:33Z
dc.date.issued	2006	de
dc.date.updated	2013-07-08	de
dc.description.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.	en
dc.identifier.other	260384798	de
dc.identifier.uri	http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-25211	de
dc.identifier.uri	http://elib.uni-stuttgart.de/handle/11682/2584
dc.identifier.uri	http://dx.doi.org/10.18419/opus-2567
dc.language.iso	en	de
dc.relation.ispartofseries	Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik;2006,2	de
dc.rights	info:eu-repo/semantics/openAccess	de
dc.subject.classification	Model checking	de
dc.subject.ddc	004	de
dc.subject.other	CEGAR	de
dc.title	Abstraction refinement with craig interpolation and symbolic pushdown systems	en
dc.type	workingPaper	de
ubs.fakultaet	Fakultät Informatik, Elektrotechnik und Informationstechnik	de
ubs.institut	Institut für Formale Methoden der Informatik	de
ubs.opusid	2521	de
ubs.publikation.typ	Arbeitspapier	de
ubs.schriftenreihe.name	Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik	de

Files

Original bundle

Now showing 1 - 1 of 1

Name:: TR_2006_02.pdf
Size:: 219.29 KB
Format:: Adobe Portable Document Format

Download

Collections

05 Fakultät Informatik, Elektrotechnik und Informationstechnik