Reference: Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005. Abstract: This thesis adapts the paradigm of CEGAR (counterexample-guided abstraction refinement) to the model checking of pushdown systems. A theoretical framework based on Craig interpolation is developed and applied to the automatic abstraction of sequential programs. It is generalized to handle full pushdown systems, including recursion, as well as multiple counterexamples. It is shown that this theory provides a framework for different heuristics to compute relevant predicates. Several concrete heuristics are proposed and discussed. An implementation based on the model checker Moped gives evidence of the usefulness of the developed concepts. In contrast to other approaches, Binary Decision Diagrams (BDDs) are used throughout the CEGAR loop. Suggested BibTeX entry: @mastersthesis{Kie05,     author = {Stefan Kiefer},     school = {Universit\"{a}t Stuttgart},     title = {Abstraction Refinement for Pushdown Systems},     year = {2005} }

GZipped PostScript (329 kB) PDF (557 kB) Slides