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.     «

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...     »

Die Arbeit untersucht einen Ansatz zur automatischen Softwareverifikation, der auf Pushdown-Systemen basiert. Pushdown-Systeme sind (vereinfacht gesagt) Transitionssysteme, deren Zustände einen Keller unbegrenzter Länge beinhalten; es besteht eine natürliche Beziehung zwischen diesen Systemen und Programmen mit rekursiven Prozeduren. Die Arbeit untersucht Model-Checking-Probleme auf Pushdown-Systemen, wobei sie zuvor bekannte Algorithmen verbessert, sowohl in asymptotischer Hinsicht als auch mit Blick auf praktische Verwendbarkeit. Die verbesserten Algorithmen werden in einem Werkzeug namens Moped verwendet. Moped ist ein Model-Checker für Linearzeitlogik (LTL) auf Pushdown-Systemen. Es kombiniert zwei unterschiedliche symbolische Techniken: automatentheoretische Ansätze werden benutzt, um den unendlichen Zustandsraum zu handhaben, der durch die Kontrolle eines Programms entsteht, und binäre Entscheidungsdiagramme (BDDs), um das Problem der Zustandsexplosion zu lindern, welches von der Repräsentation der Daten herrührt. Es wird anhand mehrerer Beispiele aufgezeigt, wie das so entstandene System benutzt werden kann, um Eigenschaften von Programmen mit rekursiven Prozeduren zu verifizieren. Darüberhinaus wurde Moped an automatisch erzeugten Abstraktionen einiger großer C-Programme getestet. Die Arbeit untersucht ebenfalls einige Optimierungen, mit denen die Effizienz des Model-Checkers gesteigert werden konnte.     «

Die Arbeit untersucht einen Ansatz zur automatischen Softwareverifikation, der auf Pushdown-Systemen basiert. Pushdown-Systeme sind (vereinfacht gesagt) Transitionssysteme, deren Zustände einen Keller unbegrenzter Länge beinhalten; es besteht eine natürliche Beziehung zwischen diesen Systemen und Programmen mit rekursiven Prozeduren. Die Arbeit untersucht Model-Checking-Probleme auf Pushdown-Systemen, wobei sie zuvor bekannte Algorithmen verbessert, sowohl in asymptotischer Hinsicht als auch mi...     »