Note: This list is currently being revised and does not claim to be complete.
Habilitation thesis
Logic and Abstraction, Verification and Falsification
Author: Jan-Georg Smaus (November 2008)
Download: (PDF)The works collected in this habilitation are concerned with the use of logic and abstraction techniques for the purpose of verifying and falsifying transition systems. The works have been structured into two main themes.
For the first theme, the transition systems in question are programs, in particular logic programs. Various aspects of correctness of such programs are considered. One aspect is termination; several contributions concerning methods for proving termination are contained in this habilitation. Another aspect is type safety, where this habilitation contains results extending the type systems for which type safety can be guaranteed.
For the second theme, the transition systems in question are timed and hybrid systems. Heuristic methods for detecting error paths in such systems are presented, which is important for supporting the design process of the systems. Another contribution is a method for representing propositional formulas compactly as a set of linear pseudo-Boolean constraints, which is useful, among other reasons, because propositional logic plays a prominent role in the analysis of transition systems, namely in the field of bounded model checking.
Habilitation thesis
Automated Planning: Algorithms and Complexity
Author: Jussi Rintanen (December 2005)
Habilitation thesis
IPP: A Planning System for ADL and Resource-Constrained
Planning Problems
Author: Jana Koehler (January 2000)
