Um der zunehmenden Komplexität von Computerprogrammen gewachsen zu bleiben, benötigen Programmierer Hilfsmittel. Sie bedienen sich automatischer Analyse-Tools, also weiterer Programme, die die neuerstellte Software auf ihre Richtigkeit überprüfen. Das ergibt allerdings ein neues Problem: Was tun, wenn das Analyseprogramm selbst fehlerhaft ist? Was wenn es ein fehlerhaftes Programm in einem sicherheitskritischen Bereich - in Fahrzeugen oder der Medizintechnik - als sicher erachtet?

René Thiemann hat eine Antwort auf diese Fragen. Der Informatiker der Computational Logic Group am Institut für Informatik der Universität Innsbruck entwickelt sogenannte Zertifizierer, die die Ergebnisse der Kontrollprogramme auf Herz und Nieren prüfen sollen. Für seine Arbeit ist der 1976 in Stadtlohn in Deutschland geborene Forscher heuer mit einem Start-Preis des Wissenschaftsfonds FWF ausgezeichnet worden.

"Im Wesentlichen geht es darum, dass ich den automatischen Analysetools nicht mehr traue", sagt Thiemann. Diese Tools haben die Aufgabe, Beweise zu generieren. Beweise, die klarstellen, dass alle Berechnungen zu einem Ergebnis führen und sich in keinen Endlosschleifen verfangen, und die über Rechenzeit und Speicherverbrauch Auskunft geben. Ein Zertifizierer kontrolliert nun als drittes Programm diese Beweise, die von den Analyseprogrammen ausgegeben werden. Erachtet es den Beweis als schlüssig, ist das Ergebnis des Analyseprogramms korrekt.

Der Haken dabei: Die Erstellung eines Zertifizierers bedeutet mühsame und langwierige Arbeit, muss doch die korrekte Funktionsweise des Programms selbst formal bewiesen werden. "Die formalen Korrektheitsbeweise der Zertifizierer können sehr komplex sein. Das Programm hat vielleicht nur 30.000 Zeilen. Es kann aber sein, dass der Beweis 130.000 Zeilen lang ist", sagt der Informatiker. Diese Arbeit will Thiemann für Terminierungs- und Komplexitätsbeweise für zwei verbreitete Programmiersprachen, Haskell und Java, in Angriff nehmen.

Effizienz und Klarheit

Die objektorientierte Programmiersprache Java steht etwa hinter Android-Apps oder Webmail-Diensten. Die funktionale Programmiersprache Haskell zeichnet sich durch ihre Effizienz und Klarheit aus und wird etwa in der Forschung eingesetzt. Bisher seien Zertifizierer, so Thiemann, lediglich bei Programmiersprachen zum Einsatz gekommen, die vornehmlich theoretischen Interessen dienen. Die Ausweitung ihrer Anwendbarkeit soll die neuen Beweisprüfer für die tägliche Praxis der Programmierer relevant machen.

Thiemann, der in Aachen promoviert hat, ist 2007 nach Innsbruck gekommen. Das Interesse an Mathematik sei immer schon da gewiesen, sagt er. Im Lauf seiner wissenschaftlichen Karriere sei er zwischen den Anwendungen der praktischen und der theoretischen Informatik gependelt. Er hat mitverfolgt, wie die automatischen Analysetools, mit denen er sich schon lange beschäftigt, immer "mächtiger und damit fehleranfälliger" wurden. Mit einem ersten Zertifizierer, den er in den vergangenen Jahren entwickelte, habe er bereits viel Erfolg gehabt. Der Start-Preis schafft für ihn nun gute Perspektiven, dieses Werkzeug auch für die Praxis aufbereiten zu können. "Das wird eine spannende Sache werden", sagt Thiemann. (Alois Pumhösel, DER STANDARD, 6.8.2014)