Abstraction refinement with craig interpolation and symbolic pushdown systems

Esparza, Javier; Kiefer, Stefan; Schwoon, Stefan

Bitte benutzen Sie diese Kennung, um auf die Ressource zu verweisen: http://dx.doi.org/10.18419/opus-2567

Langanzeige der Metadaten

DC Element	Wert	Sprache
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.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.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.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
dc.date.updated	2013-07-08	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
Enthalten in den Sammlungen:	05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Dateien zu dieser Ressource:

Datei	Beschreibung	Größe	Format
TR_2006_02.pdf		219,29 kB	Adobe PDF	Öffnen/Anzeigen

Zur Kurzanzeige

Alle Ressourcen in diesem Repositorium sind urheberrechtlich geschützt.

Universität Stuttgart

OPUS - Online Publikationen der Universität Stuttgart