Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Abstraction Refinement for Pushdown Systems


Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005.


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:

    author = {Stefan Kiefer},
    school = {Universit\"{a}t Stuttgart},
    title = {Abstraction Refinement for Pushdown Systems},
    year = {2005}

GZipped PostScript (329 kB)
PDF (557 kB)