




Publications  ModelChecking Pushdown Systems





Reference:
Stefan Schwoon. Modelchecking 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 modelchecking 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 modelchecker for lineartime logic (LTL) on pushdown systems. Two different symbolic techniques are combined to make the modelchecking feasible: automatabased 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 = {ModelChecking Pushdown Systems},
year = {2002}
}




