René Thiemann ist Professor am Institut für Informatik der Universität Innsbruck. Seine Forschungsschwerpunkt ist di grundlegenden Analyse von Softwareprogrammen.
Woran arbeiten Sie zur Zeit?
Mein Team und ich arbeiten an der Entwicklung von verifizierter Software. Verifiziert bedeutet dabei, dass die Korrektheit unserer Software mit mathematischen Beweisen formal nachgewiesen wurde. Dazu benutzen wir den Theorem-Beweiser Isabelle.
Unter anderem wird unsere verifizierte Software dazu eingesetzt, die Ergebnisse anderer nicht-verifizierter Analyse-Software zu validieren. Durch diese Validierung wurden schon Fehler aufgespürt, die über mehrere Jahre unentdeckt geblieben sind, sei es in der Software selber, oder auch in Artikeln in Fachbüchern.
Was ist für Sie Informatik?
Mathematik, die man auch noch auf dem Computer ausführen kann, anstatt von Hand zu rechnen.
Was sind für Sie Herausforderungen der Gegenwart, bei denen Informatik helfen kann?
Ich denke, die Informatik sollte bei ihren Anwendern ein Bewusstsein erschaffen, dass unverifizierte Software nicht unfehlbar ist, und somit mit Vorsicht einzusetzen ist. Nehmen wir als Beispiel den Aktienmarkt, auf dem eine Software die Transaktionen steuert. Dabei ist vorgeschrieben, dass diese Software immer dem besten Gebot den Zuschlag geben muss. Grant Passmore hat hier mit Hilfe formaler Verifikation nachgewiesen, dass es für manche real eingesetzte Software Gebote A, B und C gibt, so dass A besser bewertet wird als B, B besser als C, und C besser als A, wo also schon die Bewertungsfunktion fehlerhaft ist, da sie nicht immer ein bestes Gebot definiert.
Um diesem und ähnlichen Problem entgegenzuwirken, müssen zwei große Hürden überwunden werden: Erstens muss der Aufwand für formale Korrektheitsbeweise auf ein annehmbares Maß reduziert werden. Zweitens müssen Anforderungen an Software formal und möglichst frei von Widersprüchen spezifiziert werden.
Die Relevanz von formalen Korrektheitsbeweisen wurde erst kürzlich wieder verdeutlicht, denn der diesjährige deutsche Jugend-Forscht Preis für eine außergewöhnliche Arbeit wurde für den formalen Nachweis von der Unlösbarkeit von Hilberts 10. Problem in Isabelle verliehen.
Was haben Sie in der Auseinandersetzung mit Informatik gelernt?
Dass es immer wieder neue spannende Themen und Fragestellungen in der Informatik zu entdecken gibt.
Warum sollten sich StudentInnen für Informatik entscheiden?
Neben den hervorragenden Berufsaussichten bietet und benötigt die Informatik Kreativität, Präzision und Abstraktionsvermögen. Ähnlich wie bei Lego-Steinen, wo man aus einer kleinen Auswahl von Basis-Blöcken Kunstwerke erstellen kann, oder wie in der Mathematik aus wenigen Axiomen komplexe Beweise erstellt werden, so wird auch in der Informatik aus ein paar Basis-Operationen komplexe Software erstellt.
