Ständig verlassen wir uns auf Computerprogramme – wenn wir mit dem Handy im Internet surfen, wenn wir die Bordelektronik eines Autos nutzen, oder sogar wenn wir Lift fahren. Gleichzeitig wissen wir, dass Programme immer wieder fehlerhaft sind. Für uns Menschen ist es durch bloßes Hinsehen oft kaum möglich, jedes denkbare unerwünschte Verhalten eines Computerprogrammes zu erkennen. Aber warum sollte man dann solche Analyse-Aufgaben dann nicht automatisieren, wie so vieles andere auch?

Die Informatikerin Laura Kovacs ist Professorin an der Chalmers University in Göteborg und an der TU Wien. Sie untersucht, wie man mit Computer-Algorithmen andere Computer-Algorithmen analysieren, abstrahieren und letzten Endes verbessern kann. Dazu verwendet sie Methoden aus der Mathematik und der Logik.

Das Computerprogramm als Formel

"In einem ersten Schritt wird der Computercode in die Sprache der Logik übersetzt", erklärt Laura Kovacs. Das Programm wird in eine Formel umgewandelt, deren Eigenschaften der Computer dann automatisch überprüfen kann. Eine Eigenschaft des Programms könnte zum Beispiel die Art sein, wie sich der Wert einer Variable im Lauf der Zeit verändert. Der Computer kann etwa erkennen, dass bestimmte Variablen immer nur positive Zahlen annehmen werden.
"Nehmen wir an, der Computer untersucht ein Programm, das die Zahlen der Fibonacci-Reihe berechnet", sagt Laura Kovacs. "Die Fibonacci-Zahlen entwickeln sich nach bestimmten mathematischen Gesetzen, und genau diese Entwicklung kann der Computer automatisch erkennen."

Wenn zwei Personen unabhängig voneinander Programme schreiben, die eine Fibonacci-Reihe ausgeben können, sehen die Zeilen des Programmcodes möglicherweise völlig unterschiedlich aus – aber wenn man die Eigenschaften einer abstrahierten Version des Programmes untersucht, dann lässt sich erkennen, dass beide Programme ein ganz ähnliches Verhalten zeigen.

Auf diese Weise kann es gelingen, denn Sinn und die Funktionsweise von Programmcodes zu ergründen. Auch Fehler lassen sich dadurch vermeiden. "Es geschieht immer wieder, dass ein Programm auf Speicherorte zugreift, die es gar nicht gibt, dann kommt es oft zum Programmabsturz", sagt Laura Kovacs. "Mit unseren Methoden kann man auch angeben, welche Speicherorte vom Programmcode überhaupt jemals aufgerufen werden können – auch das ist eine Eigenschaft des Codes, die sich berechnen lässt." Auf diesem Gebiet arbeitet Laura Kovacs auch mit Microsoft Research zusammen. Logik-Methoden in der Informatik spielen in der Softwareindustrie heute eine wichtige Rolle.

Internationale Karriere und große Auszeichnungen

Für ihre Forschung erhielt Kovacs kürzlich zwei hochdotierte Preise: Einen Starting Grant des European Research Council (ERC) und den Förderpreis der Wallenberg-Stiftung. Etwa drei Millionen Euro stehen ihr damit nun zur Verstärkung ihres Teams zur Verfügung.

Laura Kovacs ist Ungarin und wurde in Temesvar (Timisoara) in Rumänien geboren, wo sie auch studierte. Für ihre Dissertation wechselte sie dann nach Österreich und promovierte am RISC an der JKU Linz. Es folgten Postdoc-Stellen in Lausanne und an der ETH in Zürich, dann kam sie als Hertha-Firnberg-Stipendiatin an die TU Wien. Derzeit ist sie Professorin an der Chalmers Universität in Göteborg, hat aber gleichzeitig auch eine Teilzeitanstellung an der TU Wien, wo sie nach wie vor Studierende betreut.

Neben den großen wissenschaftlichen Erfolgen durfte sich Laura Kovacs im vergangenen Jahr auch über privates Glück freuen: Im Sommer 2014 kam ihre Tochter zur Welt. "Karriere und Familie sind in Schweden gut zu vereinen", betont Kovacs. "Man kommt mir dort wirklich sehr entgegen, sodass am Ende weder die Wissenschaft noch die Tochter zu kurz kommt. Vom schwedischen System könnte man in Österreich noch einiges lernen."