LMU-Forscher gewinnen internationalen Wettbewerb

Ziel des Wettbewerbs ist es, den technologischen Fortschritt bei der automatisierten Suche nach Fehlern in Software voranzutreiben. Die Vermeidung von Softwarefehlern ist inzwischen überall im gesellschaftlichen Leben von großer Bedeutung. Von der korrekten Funktion von Autos, Flugzeugen, Maschinen und Haushaltsgeräten hängt viel ab – vor allem Sicherheit. „Wenn die Steuerungs-Software etwa in Autos, Flugzeugen oder bei der Energieversorgung versagt, müssen wir mit Katastrophen oder zumindest unkalkulierbaren Folgekosten für Wirtschaft und Gesellschaft rechnen“, erläutert Professor Dirk Beyer, der den Lehrstuhl „Software and Computational Systems“ am Institut der Informatik leitet. Sein Lehrstuhl ist eine der weltweit führenden Forschungsgruppen im Bereich der automatisierten Softwareverifikation. Ihm geht es darum, Werkzeuge zu entwickeln, die vollautomatisch Software-Programme untersuchen und deren Korrektheit beweisen oder eben Programmierfehler, sogenannte Software-Bugs, zu finden.

Aufgrund der Größe und Komplexität heutiger Computerprogramme ist es praktisch unmöglich, alle Fehler manuell ausfindig zu machen. „Aber auch die besten Programmierer machen Fehler, daher gewinnt die automatisierte Überprüfung von Software immer mehr an Bedeutung.“ Die Münchener Forscher um Professor Beyer entwickeln in einem breit angelegten, internationalen Open-Source-Projekt ein Analysesystem für Softwareprogramme. Dieses Analysesystem „CPAchecker“ steht auch den Studierenden zur Verfügung, die sich im Rahmen von Studienprojekten, Seminar-, Bachelor- oder Masterarbeiten direkt mit der modernsten Verifikationstechnologie vertraut machen können und sich auch in das Forschungsprojekt einbringen können. Der Lehrstuhl trat mit dem „CPAchecker“ bereits zum siebten Mal bei der International Competition on Software Verification an: diesmal in Thessaloniki, Griechenland, wobei sich CPAchecker gegen 20 andere Teams durchgesetzt hat. In drei von acht Programmkategorien erreichten die Münchener den ersten Platz, in zwei Kategorien den zweiten und in einer weiteren Kategorie den dritten Platz. Am wichtigsten ist die Gesamtwertung, bei dem das LMU-Team Sieger wurde und damit weiterhin zu den renommiertesten Verifikationsgruppen weltweit gehört. Auch bei den Wettbewerben 2012 bis 2017 erreichte die Gruppe sehr gute Ergebnisse und ist zudem mit der Gödel-Medaille der Österreichischen Kurt-Gödel-Gesellschaft für ihre Leistung ausgezeichnet worden. Die International Competition on Software Verification wird seit 2012 im Rahmen der internationalen Algorithmen-Konferenz TACAS ausgetragen und teilweise von Firmen wie Microsoft und Amazon finanziell unterstützt.

Bei dem Wettbewerb konkurrieren internationale Forscherteams darum, in gegebenen Computerprogrammen Fehler zu finden oder aber deren Korrektheit zu beweisen. In diesem Jahr wurden insgesamt 9.523 Verifikationsaufgaben vollautomatisiert bearbeitet. Die Bewertung der Ergebnisse erfolgte durch eine 22-köpfige Jury internationaler Experten von Universitäten und Unternehmen aus Australien, Brasilien, China, Deutschland, Großbritannien, Indien, Russland und Tschechien. Für den Wettbewerb sind enorme Rechenkapazitäten erforderlich; hierzu wurden Server der LMU genutzt. „Den Rechencluster des Lehrstuhls kann man sich von der Größe her wie einen überdimensionierten Kleiderschrank vorstellen“, so Beyer. Mit knapp 1.600 Recheneinheiten und mehr als fünf Terabyte Hauptspeicher wird dieser als eigene Einheit im klimatisierten Bereich des Rechenzentrums der Rechnerbetriebsgruppe des Instituts für Informatik der LMU betrieben. „Für eine vollständige Serie von Experimenten, wie sie zum Beispiel für eine wissenschaftliche Publikation erforderlich ist, ist ein Forscher aufgrund der Rechenzeit eine ganze Woche beschäftigt. Der große Rechencluster hilft uns, weiterhin Forschung auf internationalem Spitzenniveau betreiben zu können und attraktiv für internationale Studierende und hochrangige Forschungskooperationen zu sein“, ergänzt Professor Beyer.