Selected publications by Stefan Schwoon

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.

@phdthesis{schwoon-phd02,
   author = {Schwoon, Stefan},
   month = jun,
   school = {Technische Universit{\"a}t M{\"u}nchen},
   type = {{Ph.}{D.} {T}hesis},
   title = {Model-Checking Pushdown Systems},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schwoon-phd02.pdf},
   year = {2002},
}

About LSV