My current research is concerned with formal methods and software verification. I have worked on applications in robotics, program certification, abstraction and reuse of formal program develpoments, and user interfaces for theorem provers and formal method tools.

Past and Present Highlights

Previous Work

In my thesis, I developeded a compositional semantics for term rewriting systems which is based on the theory of enriched monads. This grew into a wider initiative to use methods from category theory in term rewriting, spear-headed by Neil Ghani and his group, now at the University of Strathclyde.

After arriving in Bremen, together with other colleagues we developed various tools to support formal program development, such as the transformation system TAS and various extensions for the tactical theorem prover Isabelle, including a graphical user interface. My habilitation gives a good overview of my research in those years (1998-- 2005).