Der Mann mit dem Microsoft-Stipendium

Adrian Hoffmann

Thomas Wies, Informatikstudent in Freiburg, hat ein Microsoft-Stipendium bekommen, das mit 90.000 dotiert ist. Er freut sich, aber er gibt sich ganz bescheiden. Im Interview hat er uns ein bisschen was über sich erzählt, und das komplizierte Thema seiner Promotionsarbeit uns noch mal ausführlich in einer Mail erklärt.



So sieht also Bill Gates Nachfolger aus.

Thomas: Naja, nicht ganz. Bill Gates hat übrigens sein Studium abgebrochen...

Das heißt also, du bist noch besser?

Thomas: Nee. Irgendwann muss man sich halt entscheiden. Entweder man bleibt bei der Forschung oder man versucht echtes Geld zu verdienen.

Zu welchem Typ gehörst du?

Thomas: Ich will in der Forschung bleiben.

Wie hast du denn reagiert, als du von diesem Stipendium erfahren hast?

Thomas: Ich war schon ziemlich überrascht. Da bewerben sich eine Menge Leute aus ganz Europa. Aus meiner Sicht ist es eigentlich wie ein Lottogewinn.

90.000 Euro - das hört sich nach einer ordentlichen Unterstützung an!

Thomas: Bisher hatte ich ein Stipendium über ca. 1500 Euro im Monat. Das ist schon ein Unterschied. Es ist ein gutes Gehalt, rechnet man es auf die Laufzeit von drei Jahren.

Wie ist es eigentlich dazu gekommen, dass du dich für dieses Stipendium beworben hast?

Thomas: Mein Doktorvater Professor Podelski hat mich darauf aufmerksam gemacht. Man muss gewisse Referenzen haben, um dafür infrage zu kommen. Außerdem haben fünf Gutachter mein Promotionsthema bewertet.

Was hat Microsoft davon, dir ein 90.000-Euro-Stipendium zu geben?

Thomas: Ich denke, da spielt schon eine große Rolle, dass sie an potentiellem Nachwuchs interessiert sind.

Also, sorry, aber mit dem Geld würde ich mir einen Porsche kaufen, einen 911er. Und du?

Thomas: Ich muss doch auch von etwas leben. Das reicht gut aus, aber mehr nicht. Ich verdiene ja nebenher nichts.

Wie sieht deine Arbeit eigentlich genau aus - was machst du den ganzen Tag?

Thomas: Es ist viel Theoretisches dabei, viel Bleistift- und Papierarbeit, aber auch viel Praxis. Man entwickelt neue Verfahren auf dem Papier. Dann versuchen wir hier unsere Ideen zu implementieren, Programmierung also. Außerdem ist man auch in ständigem Austausch mit anderen Wissenschaftlern. Wir arbeiten zum Beispiel mit einem Team am MIT in Boston zusammen.

Worum geht es denn jetzt genau in deinem Promotionsthema?

Thomas: Einfach ausgedrückt geht es darum die Fehlerfreiheit von Programmen zu garantieren, bzw. Fehler automatisch zu finden. Solche Fehler wie den Bluescreen zum Beispiel, dem man aus alten Windowszeiten kennt. Es geht um Programme, die die Ursache eines Fehlers in einer Software suchen. Das ist ziemlich kompliziert, weshalb ich es noch mal ausführlich in einer Mail erklären werde. Es ist ein sehr großes Forschungsgebiet.

Ich stelle mir es ziemlich schwierig vor, als Informatiker auf einer Party den anderen Gästen zu erzählen, was ich beruflich genau mache. Wie ist das?

Thomas: Ja, das ist schon so. Meistens mache ich es recht dramatisch, ich sage ganz konkret, was für Folgen meine Arbeit haben kann. Es macht Betriebssysteme einfach sicherer, oder zum Beispiel die Software eines Flugzeuges oder eines Autos, es gibt da so viele Beispiele.

Wo siehst du dich denn in ein paar Jahren beruflich?

Thomas: Ich würde schon gerne im Akademischen bleiben.

Also kein Bill Gates?

Thomas: Nein.



Thomas' Promotionsthema, von ihm selbst erklärt:

Jeder, der schon einmal an einem Computer gearbeitet hat, hat sicherlich auch schon die leidvolle Erfahrung gemacht, dass ein Programm oder der Computer selbst mit einer kryptischen Fehlermeldung abgestürzt ist. Solche Abstürze werden durch Programmierfehler in der Software, das heißt einer Anwendung oder dem Betriebssystem, verursacht. Programmabstürze sind zwar nervenaufreibend, zählen aber noch zu den eher harmlosen Folgen solcher Fehler. In den Zeiten des Internets stellen sie auch ein ernstes Sicherheitsrisiko dar, denn sie werden systematisch ausgenutzt, um über das Internet unbemerkt Daten des Benutzers auszuspähen oder Schadsoftware wie Viren und Trojaner auf dem betroffenen Computer zu installieren.

Um Fehler bereits vor Auslieferung der Software zu beheben, wird sie während ihrer Entwicklung ausgiebig getestet. Die Komplexität von Software erlaubt es aber nicht, allein durch Testen alle Fehler zu finden. Wie kann man also Fehlerfreiheit garantieren? Die Informatik und speziell unser Lehrstuhl versuchen dies systematisch, durch Anwendung formaler, mathematischer Methoden zu erreichen. Dabei entwickeln wir Werkzeuge, die Fehler in Programmen automatisch aufspüren und bei deren Abwesenheit einen mathematischen Beweis erbringen, der die Fehlerfreiheit formal bestätigt.

Bereits heute halten diese Methoden Einzug in die industrielle Softwareentwicklung. Zum Beispiel hat Microsoft Research ein Werkzeug zur Verifikation von Software konstruiert, das bei der Entwicklung der nächsten Generation des Betriebssystems Windows zum Einsatz kam.

Dabei haben sich auch die Grenzen des aktuellen Forschungsstands gezeigt. Eines der offenen Probleme ist die Analyse von Programmen, die Datenstrukturen in nicht-trivialer Weise verwenden.In meiner Arbeit befasse ich mich mit diesem Problem. Ich entwickle Verfahren, die erstens präzise genug sind, um solche Programme zu verifizieren und sich zweitens einfach mit den existierenden Methoden kombinieren lassen. Die wissenschaftliche Herausforderung liegt dabei in der prinzipiellen Unmöglichkeit dieses Unterfangens. Einer der fundamentalen Gesetze der Informatik hat nämlich zur Folge, dass es kein Programm geben kann, das die Fehlerfreiheit eines beliebigen anderen Programms verifiziert. Es geht also darum, dem Unmöglichen ein Schnippchen zu schlagen, das heißt Verfahren zu entwickeln, die, obwohl sie prinzipiell unvollkommen sind, die Programme verifizieren können, die tatsächlich von praktizierenden Softwareentwicklern geschrieben werden.