Prof. Dr. Heinz Peter Gumm

Arbeitsgebiet: Formale Methoden

Arbeitsschwerpunkte: Strukturtheorie zustandsbasierter Systeme (Coalgebren), Theorie und Werkzeuge zur Verifikation von Programmen und Protokollen, Universelle Algebra und Logik.

1. Zustandsbasierte Systeme treten in allen Bereichen der Informatik auf. Der einfachste Typ besteht aus einem System, das in Abhängigkeit von seinem internen Zustand auf einen Input reagiert. Dabei wird ein Output produziert, und gleichzeitig ändert sich der interne Zustand. Solche und allgemeine Beispiele finden sich in der Theorie der Programmiersprachen, im Compilerbau, im objekt-orientierten, im funktionalen und im verteilten Programmieren. Spezifikationen derartiger Systeme sind nur an dem Input-Outputverhalten interessiert, der interne Zustand ist nicht beobachtbar, obwohl er für das Funktionieren des Systems entscheidend ist. Wir entwickeln eine Theorie solcher und allgemeinerer zustandsbasierter Systeme, so genannter Coalgebren. Insbesondere ist von Interesse, universelle Systeme zu konstruieren, das sind solche, die bei einer minimalen Anzahl von Zuständen alle möglichen beobachtbaren Verhaltensweisen beinhalten.

2. An die Zuverlässigkeit von Software und Hardware in sicherheitskritischen Anwendungen (etwa in der Verkehrstechnik) werden besonders hohe Anforderungen gestellt. Bei verteilten Programmen und Protokollen insbesondere ist ein Aufspüren von Fehlern durch Testläufe nahezu hoffnungslos. Daher bedient man sich mathematischer Methoden, um die Korrektheit zu zeigen: Der Nachweis, dass ein Programm eine Spezifikation erfüllt, verläuft analog zum Beweis eines mathematischen Satzes. Für die Überprüfung einer Vielzahl von Teilbehauptungen sind maschinelle Verifikationswerkzeuge unerlässlich. Wir beschäftigen uns mit der Konstruktion und Anwendung solcher Verifikationssysteme sowie den zugehörigen mathematischen Grundlagen, die enge Bezüge zu Algebra und formaler Logik aufweisen.

3. Universelle Algebra und Logik sind Grundlagenwissenschaften, die einen geeigneten mathematischen Hintergrund für viele Gebiete der Informatik bereitstellen. Die Universelle Algebra ist der theoretische Hintergrund abstrakter Datentypen, und liefert Anhaltspunkte für die Ausgestaltung der oben erwähnten Theorie der Coalgebren. Verschiedene logische Systeme liefern Sprachen und Beweismethoden für die formalen Kalküle der Programmverifikation.

Homepage: www.informatik.uni-marburg.de/~gumm

Sprechstunde: Donnerstag, 16-18 Uhr