Jan-Georg Smaus, Albert-Ludwigs-Universitat Freiburg, Germany
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.