Alle möglichen Fälle eines Programms

Florian Zuleger erstellt mathematische Modelle von Softwareanwendungen

Wie lange braucht eine Software, um die an sie gestellten Aufgaben zu erfüllen? Welche Ressourcen, wie viel Arbeitsspeicher, Rechenleistung, Internet-Bandbreite braucht das Computerprogramm dabei? Kommt die Anwendung mit beschränkten Kapazitäten, etwa auf einem Smartphone, aus? - Fragen, die sich Florian Zuleger bei seinen Forschungen im Bereich der Programmanalyse am Institut für Informationssysteme an der TU Wien stellt.

Natürlich könnte man auch etwas über das Programm herausfinden, indem man es laufen lässt, und sich ansieht wie viel Zeit und Platz es braucht, räumt Zuleger ein. "Das ist ein legitimer Ansatz, bei dem man gute Informationen erzielen kann." Software, egal ob sie am Smartphone das Wetter anzeigt oder einen Industrieroboter steuert, läuft aber nicht in jedem Fall gleich ab. Wenn man andere Daten eingibt, verhält sie sich auch anders, sagt Zuleger. Und wenn man Sicherheit haben will, dass ein Programm nicht mehr Zeit als veranschlagt benötigt, wenn man die Garantie haben will, dass alle möglichen Fälle der Programmausführung in der Analyse berücksichtigt sind, reicht es nicht aus, das Programm einfach laufen zu lassen.

"Wir zielen also darauf ab, dass man statisch herausfindet, wie lange das Programm braucht - ohne dass man es startet", erklärt Zuleger. Das bedeutet, dass man ein neues Programm braucht: "Man muss eine Software schreiben, die das Programm analysiert, modelliert und die Eigenschaften überprüft." Die Analyse des Programms erfolgt, indem es mathematisch beschrieben wird. Anhand des mathematischen Modells zieht man dann seine Schlüsse und sucht die Eigenschaften des untersuchten Programms am Modell zu beweisen.

Für seine Ansätze bei der automatischen Analyse der Komplexität und Laufzeit von Software wurde Zuleger heuer ein Grant des Wiener Technologiefonds WWTF zugesprochen, was seine Forschungen im Arbeitsbereich Formal Methods in Systems Engineering an der TU Wien zumindest auf vier Jahre sichert. In dieser Zeit will er sein Projekt erweitern und sich neben der Weiterentwicklung der Grundlagen darauf konzentrieren, sie auch tatsächlich in Software-Tools umzusetzen, die ökonomisch verwertbar sind - aber erst, "wenn die Methoden eine gewisse Reife erlangt haben".

Zuleger kommt ursprünglich aus der Mathematik. Das Studium derselben war eine logische Konsequenz: "Ich kann nicht sagen, wann das angefangen hat. Die Mathematik hat mich immer interessiert." Später fand er im Fachbereich der Formalen Methoden, zu denen die Programmanalyse gehört, ein "schönes Thema an der Schnittstelle von Mathematik und Informatik".

Der heute 28-Jährige kommt ursprünglich aus München. Seinem Doktorvater Helmut Veith, der 2009 der Ruf an die TU Wien ereilte, ist er nach Österreich gefolgt. Der deutsch-österreichische Culture-Clash ist für den Bayern weniger schlimm: Aus der Außensicht sei es besonders interessant, Österreichern beim Verfolgen eines Fußballspiels mit deutscher, aber ohne österreichische Beteiligung zuzuschauen. "Da ist die Hälfte gegen, die Hälfte für Deutschland." Ihm gegenüber reißen sich die Österreicher offenbar zusammen: "'Piefke' gibt's zwar manchmal. Ich bin aber insgesamt zufrieden mit dem nachbarschaftlichen Verhältnis." (Alois Pumhösel/DER STANDARD, 3. 10. 2012)