Research
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
- In
the SELFIE
project, we develop the notion of self-verifying systems, together
with a suitable architecture and development methodology.
Funded by the German Federal Ministry for Education and Research, 2016-2019 - In the SPECifIC
project, we have developed a novel design flow for cyber-physical systems,
characterised by natural-language techniques for requirement
specification, a novel formal specification layer, comprehensive tool
support throughout the development process, and functional change
management.
Funded by the German Federal Ministry for Education and Research, 2013-2016 - In the IGEL project, we
developed the safety-directed software for a safe cone laser
rangefinder. The key algorithm was reviewed by TÜV Nord, and the
demonstrator was presented on the 2012 Hannover fair.
Funded by the German Federal Ministry for Education and Research, 2010-2011 - In the SAMS
project, we designed, implemented and formally verified a collision
avoidance algorithm for autonomous service robots. The conformance of
the development to the relevant standard, IEC 61508, was certified by
TÜV Süd GmbH. This is one of the first applications of formal methods
to service robotics.
Funded by the German Federal Ministry for Education and Research, 2006- 2009 - In the AWE project, we investigated methods
for the systematic abstraction and reuse of formal program developments and
proofs. The concepts were implemented in the theorem prover Isabelle, and one
of the major results is an extension package for Isabelle with
abstraction and structuring concepts such as theory morphisms.
Funded by the German research council DFG, 2002- 2008 - Together with David Aspinall, I am working on techniques for proof engineering: how to construct, maintain and present large formal developments.
- The User Interfaces for Theorem Provers (UITP) workshop series, where I am in the steering commitee.
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).