Reference:

Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002.

Abstract:

The thesis investigates an approach to automated software verification based on pushdown systems. Pushdown systems are, roughly speaking, transition systems whose states include a stack of unbounded length; there is a natural correspondence between them and the execution sequences of programs with (possibly recursive) subroutines. The thesis examines model-checking problems for pushdown systems, improving previously known algorithms in terms of both asymptotic complexity and practical usability. The improved algorithms are used in a tool called Moped. The tool acts as a model-checker for linear-time logic (LTL) on pushdown systems. Two different symbolic techniques are combined to make the model-checking feasible: automata-based techniques are used to handle infinities raised by a program's control, and Binary Decision Diagrams (BDDs) to combat the state explosion raised by its data. It is shown how the resulting system can be used to verify properties of algorithms with recursive procedures by means of several examples. The checker has also been used on automatically derived abstractions of some large C programs. Moreover, the thesis investigates several optimizations which served to improve the efficiency of the checker.

Suggested BibTeX entry:

@phdthesis{Sch02b,
    author = {Stefan Schwoon},
    school = {Technische Universit{\"a}t M{\"u}nchen},
    title = {Model-Checking Pushdown Systems},
    year = {2002}
}