Pressemeldung der Universität Passau vom 02.07.2015

Gesamtsieg plus zwei Einzelsiege – so lautet die Erfolgsbilanz, mit der die Verifikationsforscher der Universität Passau von der International Competition on Software Verification zurückgekommen sind. Darüber hinaus erreichten die Passauer Forscher mit ihrem Verifikationswerkzeug „CPAchecker“ in den weiteren Kategorien drei zweite und zwei dritte Plätze und gewannen damit mit Abstand die meisten Medaillen unter den 22 teilnehmenden Teams aus aller Welt.

Die International Competition on Software Verification, die im Rahmen der Algorithmen-Konferenz TACAS stattfindet ist ein Wettbewerb, bei dem Wissenschaftlerinnen und Wissenschaftler darum wetteifern, in gegebenen Computerprogrammen Fehler zu finden oder aber deren Korrektheit zu beweisen. Ziel des Wettbewerbs ist es, den Fortschritt bei der Verifikation von Softwaresystemen anzutreiben. „Nie zuvor war die korrekte Funktion von Computerprogrammen so wichtig wie heute: Fast alle Bereiche des täglichen Lebens in der Gesellschaft und in der Wirtschaft sind von Computerprogrammen abhängig“, erklärt Prof. Dr. Dirk Beyer, der das Passauer Team leitet. „Jedoch macht jeder Mensch Fehler, auch Programmierer von Software. Enorm wichtig sind deshalb Computerprogramme zur Verifikation, also das automatisierte Finden von Fehlern in anderen Computerprogrammen. Dazu sind enorme Rechenkapazitäten erforderlich, und es geht letztendlich darum, mit schlauen Algorithmen die Bugs oder Beweise mit möglichst geringen Rechenressourcen zu berechnen.“

Die Passauer Gruppe hat sich mit dem Verifikationswerkzeug „CPAchecker“ beim diesjährigen Wettbewerb gegen die Konkurrenz aus 13 Ländern durchgesetzt und gehört damit weiterhin zu den renommiertesten Verifikationsgruppen weltweit. Zuletzt war die Gruppe mit der Gödel-Medaille der Österreichischen Kurt-Gödel-Gesellschaft für ihre Leistung ausgezeichnet worden. Prof. Dr. Dirk Beyer ist seit 2009 Inhaber des Lehrstuhls für Softwaresysteme, an dem kontinuierlich Beiträge zur Verbesserung der Softwarequalität geleistet werden.

Über CPAchecker

Das Verifikationswerkzeug CPAchecker wird in der Praxis angewendet, um Fehler im Linux-Kernel zu finden. Die Linux-Software findet auf zahlreichen Geräten Verbreitung, so zum Beispiel auf vielen Heim- oder Büro PCs, auf Servern in Rechenzentren, aber auch auf Netzwerk-Routern oder Android-Smartphones. Das Forschungsprojekt ist insbesondere auch für Passauer Informatik-Studierende interessant, weil Master-Studierende im Rahmen der vorlesungsbegleitenden Projekte zur Vorlesung Software-Verification oder als studentische Hilfskraft am Lehrstuhl an den CPAchecker-Projekten mitarbeiten dürfen. (Katrina Jordan)

Externer Link: www.uni-passau.de