Forschung

Eines der zentralen Ziele der Forschungsarbeiten am Lehrgebiet Theoretische Informatik ist es, theoretische und praktische Aspekte der Informatik miteinander in Verbindung zu bringen. Dabei stehen derzeit zwei Themen im Vordergrund.

Das Ziel dieser Forschungen ist der Entwurf und die Implementierung formal-logischer Verfahren zur Entwicklung zuverlässiger Software, insbesondere zuverlässiger und effizienter verteilter Systeme. Dabei geht es vor allem um die Anwendung von logischen und automatischen Beweisverfahren in der Programmsynthese, -verifikation und -optimierung.

Eine der Hauptanwendungen der letzten Jahre war die Entwicklung einer logischen Programmierumgebung für das ENSEMBLE Kommunikationssystem. In Zusammenarbeit mit Forschern der Cornell University haben wir Verfahren entwickelt, die den gesamten Code von ENSEMBLE in die Logik des Beweissystems NUPRL einbetten, sicherheitskritische Eigenschaften von ENSEMBLE innerhalb von NUPRL überprüfen, die Effizienz von ENSEMBLE durch den Einsatz wissensbasierter Optimierungstechniken signifikant (d.h. um den Faktor 3-5) verbessern und dabei einen Beweis für die Korrekheit der Optimierung generieren.

Das Ziel dieser Forschungen ist die Entwicklung vollautomatischer logischer Beweisverfahren sowie ihre Integration in interaktive Beweissysteme wie NUPRL, MetaPRL, Coq, Isabelle oder PVS. 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.

Die Forschungen der letzten Jahre konzentrierten sich dabei vor allem auf Beweissuchverfahren auf der Basis von Matrix-Charakterisierungen logischer Gültigkeit. Matrix-Charakterisierungen ermöglichen eine sehr kompakte Darstellung des Suchraums sowie eine Extraktion von Beweisobjekten zur Steuerung interaktiver Beweissysteme. Für konstruktive, modale und lineare Logiken haben wir eine uniforme Beweisprozedur entwickelt und einen Beweiser JPROVER zur Steuerung von Beweisen in NUPRL implementiert. JPROVER wird mittlerweile auch in MetaPRL und Coq eingesetzt.

In den kommenden Jahren wollen wir die Leistungsfähigkeit dieser Prozeduren durch die Integration von Induktionstechniken, Entscheidungsprozeduren, Beweisplanern, und mathematischen Wissensbanken erheblich steigern und in praktischen Anwendungen austesten.