Forschung

Ich interessiere mich für die Verwendung formaler Methoden in der Information, inbesondere beim Erstellen von sicheren und zuverlässigen Systemen. Dies umfasst Methoden und Werkzeuge zum Design, der Spezifikation, der Validierung und der Verfikation von Soft- und Hardwaresystemen.

Aktuelle Arbeiten:

• Wartung von Isabelle/HOL-Z, einer Beweisumgebung für den Spezifikationsformalismus Z. Weitere Informationen gibt es auf der HOL-Z Hompage.
• Entwicklung von Isabelle/HOL-OCL, einer Beweisumgebung für UML/OCL Spezifikationen. Weitere informationen gibt es auf der HOL-OCL Seite.
• Entwicklung von HOL-TestGen, einem Test-Daten Generator für den spezifikationsbasierten Unit-Test. Weitere informationen gibt es auf der HOL-TestGen Seite.
• Bereitstellen von IsaMorph, einer direkt lauffähigen Linux CD mit dem interaktiven Theorembeweiser Isabelle. Weitere informationen gibt es auf der IsaMorph Seite.