Seit Beginn meines Studiums ist es mein Ziel, theoretische und praktische Aspekte der Informatik miteinander in Verbindung zu bringen. Mein Interesse für den Einsatz formaler Methoden in der Programmierung richtete sich zunächst auf die Grenzen dessen, was überhaupt bzw.in akzeptabler Zeit berechnet werden kann. Nach meiner Promotion verlagerte ich meinen Schwerpunkt auf formal-logische Verfahren zur Entwicklung zuverlässiger Software - ein Gebiet in dem theoretische Grundlagen und praktische Fragestellungen gleichermaßen eine wichtige Rolle spielen.
Während meines Postdoc-Jahres an der Cornell University habe ich an
der Fertigstellung der ersten Version des Programm- und
Beweisentwicklungssystems NUPRL
(Proof/Program Refinement Language, version 
)
mitgewirkt und gründliche Einsichten in formale Logik,
Beweisverfahren und Techniken der Automatischen Programmierung gewonnen. Hierbei
wurde deutlich, daß Programmentwicklung mit logisch-formalen Methoden nur dann
praktikabel ist, wenn sie durch formal verifiziertes Wissen über die
relevanten Anwendungsbereiche und durch automatische Entwurfsstrategien
unterstützt wird.
In den Folgejahren stellte sich während meiner Forschungen im LOPS Projekt an der TU München heraus, daß auch die Entwicklung der Programmentwurfsstrategien auf formal verifiziertes Wissen gestützt werden muß. Ohne eine Formalisierung von Wissen über Programmiermethoden auf einem relativ hohen konzeptionellen Niveau sind automatische Programmsyntheseverfahren entweder extrem ineffizient oder nicht in der Lage, eine Garantie für die Zuverlässigkeit der erzeugten Software abzugeben.
An der TU Darmstadt habe ich daher begonnen, eine formale Theorie der Programmierung zu entwickeln, in der das für die Programmierung relevante Wissen formalisiert und verifiziert wird. Hierdurch wird das Niveau des formalen Schließens von logischen Kalkülen auf die in der Programmierung übliche Terminologie angehoben und somit eine Brücke zwischen formaler Logik und praktischer Anwendung geschlagen. Die Grundlagen dieses Ansatzes habe ich in meiner Habilitationsschrift ausführlich dargelegt.
Auf dieser Basis forsche ich derzeit an zwei Schwerpunktthemen. Zusammen mit meinen Doktoranden und früheren Diplomanden der TU Darmstadt arbeite ich an vollautomatischen Beweisverfahren für konstruktive, modale und lineare Logiken und Induktion, sowie an ihrer Integration in das NUPRL System. Diese Verfahren werden zur Steuerung konzeptionell einfacher, aber technisch aufwendiger Anteile von Verifikationen und Synthesen eingesetzt, was die praktischen Arbeiten mit dem Programmentwicklungssystem erheblich vereinfacht.
Zum anderen arbeite ich seit meiner Rückkehr an die Cornell-University an einer logischen Programmierumgebung für die Entwicklung zuverlässiger und effizienter verteilter Systeme. Diese Arbeiten werden durchgeführt in Kooperation mit den Entwicklern von des Kommunikations-Toolkits ENSEMBLE, einem Nachfolger des inzwischen kommerziell eingesetzten ISIS Systems. Ich habe Verfahren entwickelt, die den gesamte Code von ENSEMBLE in die formale Sprache von NUPRL einbetten und somit für die Anwendung logischer Beweis- und Transformationsverfahren bereitstellen. Sie ermöglichen es, sicherheitskritische Eigenschaften von Kommunikationssystemen in NUPRL zu überprüfen, ohne das hierfür ein tiefes Verständnis der zugrundeliegenden Logik erforderlich ist. Auf dieser Grundlage habe ich logische Verfahren zur automatischen Optimierung von ENSEMBLE-basierten Kommunikationssystemen implementiert, deren Korrektheit formal garantiert ist. Aufgrund des wissensbasierten Vorgehens kann kann der optimierte Code innerhalb von wenigen Sekunden erzeugt werden und ist in typischen Anwendungssituationen signifikant schneller als das Originalsystem.
Es ist mein Ziel, beide Richtungen zu vertiefen und durch anwendungsbezogene Arbeiten mit Beweissystemen die Brücke zwischen Theorie und Praxis weiter zu verfestigen.