You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems1

Issue title: Application of Constraints to Formal Verification

Guest editors: Miroslav N. Velev

Article type: Research Article

Authors: Esparza, Javier | Kiefer, Stefan | Schwoon, Stefan

Affiliations: Institut für Informatik, Technische Universität München, Germany. E-mails: [email protected], [email protected], [email protected]

Note: [1] This work was partially supported by the DFG project Algorithms for Software Model Checking. Parts of this work appeared in a TACAS’06 paper [5] and a Master’s thesis [11]. Most of this work was done at the Universität Stuttgart.

Keywords: model-checking, abstraction refinement, Craig interpolation, BDDs, push-down systems

DOI: 10.3233/SAT190051

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 27-56, 2009

Received 1 January 2007
|
Revision received 1 March 2008
|
Published: 1 June 2008
Get PDF open access

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 Binary Decision Diagrams (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.

Show more