Drei Mal Gold, vier Mal Silber, zwei Mal Bronze und einen zweiten Platz in der Gesamtwertung – so lautet die Erfolgsbilanz, mit der die Verifikationsforscher der Universität Passau von der International Competition on Software Verification zurückgekommen sind. Der Wettbewerb soll den technologischen Fortschritt bei der automatisierten Suche nach Fehlern in Software vorantreiben. Die Vermeidung von Softwarefehlern ist wiederum grundlegend für die Sicherheit von Anwendungen z. B. in Autos oder Flugzeugen.
„Wenn die Steuerungs-Software z. B. 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 Prof. Dr. Dirk Beyer, der die Passauer Forschungsgruppe im Bereich Softwareverifikation leitet. Aufgrund der Größe und Komplexität heutiger Computerprogramme sei es praktisch unmöglich, 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 Passauer Forscher am Lehrstuhl für Softwaresysteme von Prof. Beyer entwickeln in einem breit angelegten, internationalen Projekt ein entsprechendes Analysesystem für Softwareprogramme unter dem Namen „CPAchecker“. Auch Studierende können sich im Rahmen von Studienprojekten, Seminar-, Bachelor- oder Masterarbeiten direkt in das Forschungsprojekt einbringen.
Die Passauer Gruppe trat mit dem „CPAchecker“ bei der fünften International Competition on Software Verification in Eindhoven (Niederlande) gegen 35 Teams aus 16 Ländern an. In drei von zehn Programmkategorien erreichten die Passauer den ersten Platz, in vier Kategorien den zweiten und in weiteren zwei Kategorien den dritten Platz. In der Gesamtwertung erreichten die Passauer den zweiten Platz und gehören damit weiterhin zu den renommiertesten Verifikationsgruppen weltweit. Neben den ebenfalls sehr guten Platzierungen bei den Wettbewerben 2012 bis 2015 ist die Gruppe zudem mit der Gödel-Medaille der Österreichischen Kurt-Gödel-Gesellschaft für ihre Leistung ausgezeichnet worden.
Die International Competition on Software Verification findet seit 2012 jährlich im Rahmen der Algorithmen-Konferenz TACAS statt. Bei dem Wettbewerb konkurrieren internationale Forscherteams darum, in gegebenen Computerprogrammen Fehler zu finden oder aber deren Korrektheit zu beweisen. In diesem Jahr wurden 6.000 Computerprogramme vollautomatisiert überprüft. Die Bewertung der Ergebnisse erfolgte durch eine über 20-köpfige Jury internationaler Experten von Universitäten in Australien, Brasilien, China, Deutschland, England, Italien, Russland, Spanien, Südafrika, Taiwan, Tschechien und den USA.
Für den Wettbewerb sind enorme Rechenkapazitäten erforderlich, hierzu wurden Server der Universität Passau genutzt. „Unseren Rechencluster des Lehrstuhls kann man sich von der Größe her wie einen überdimensionierten Kleiderschrank vorstellen“, so Beyer. Mit knapp 800 Recheneinheiten und mehr als drei Terabyte Hauptspeicher wird dieser als eigene Einheit im klimatisierten Bereich des Zentrums für Informationstechnologie und Medienmanagement (ZIM) der Universität betrieben. Doch auch diese enorme Rechenpower kommt an ihre Grenzen: „Für eine vollständige Serie von Experimenten, wie sie z. B. für eine wissenschaftliche Publikation erforderlich ist, ist ein Forscher aufgrund der Rechenzeit eine ganze Woche beschäftigt. Daher planen wir momentan den Ausbau der Rechenressourcen, um auch weiterhin Forschung auf internationalem Spitzenniveau betreiben zu können und attraktiv für internationale Studierende und hochrangige Forschungskooperationen zu bleiben“, ergänzt Prof. Beyer.
