Meldung

Gödel-Medaille für Passauer Informatik-Forscher

Die Passauer Wissenschaftler Prof. Dr. Dirk Beyer, Stefan Löwe und Philipp Wendler haben für ihre Beiträge zur Erforschung effizienter Verifikationsmethoden und -algorithmen, für den Technologietransfer durch die Implementierung im Software-System CPAchecker und für ihre Verdienste beim internationalen Wettbewerb für Software-Verifikation die Gödel-Medaille erhalten.

Die Preisträger mit dem Erfinder des Model-Checking (Turing-Award 2007), Edmund M. Clarke (Mitte), der die Medaillen überreichte. Prof. Dirk Beyer (2.v.r.) und Philipp Wendler (2.v.l.).
Die Preisträger mit dem Erfinder des Model-Checking (Turing-Award 2007), Edmund M. Clarke (Mitte), der die Medaillen überreichte. Prof. Dirk Beyer (2.v.r.) und Philipp Wendler (2.v.l.).

Die Preisverleihungszeremonie fand im Rahmen des Symposiums „Wiener Sommer der Logik" statt, bei dem sich im Juli rund 2000 Logiker aus aller Welt über aktuelle Fragestellungen ihrer Disziplin austauschten. Benannt ist die Auszeichnung nach dem seinerzeit in Wien forschenden Logiker Kurt Gödel. „Kurt Gödel hat 1930 den Unvollständigkeitssatz bewiesen, der besagt, dass es in jeder genügend mächtigen Theorie Aussagen gibt, die man weder beweisen noch widerlegen kann", erklärt Dirk Beyer. „Eine Entdeckung, die die Welt der Logik damals schockiert und revolutioniert hat." Auf die Auszeichnung ist der 42-Jährige sehr stolz: „Die Kurt-Gödel-Medaille unterstreicht die Wichtigkeit sowie die Qualität unserer Forschungsarbeiten im internationalen Vergleich und rechtfertigt die Investitionen der Universität und meiner Arbeitsgruppe." Erst vor kurzem wurde am Lehrstuhl ein neuer High-Speed-Rechner in Betrieb genommen, der nun die Verifikationsforschung unterstützt.

Bei der Software-Verifikation geht es darum herauszufinden, ob ein Computer-Programm logisch korrekt arbeitet, also der angegebenen Spezifikation entspricht. "Einfach ausgedrückt wollen wir beweisen, ob der Satz 'Das Programm erfüllt seine Spezifikation' wahr ist oder falsch", so Dirk Beyer. "Ist die Spezifikation nicht erfüllt, so enthält das das Programm einen Programmierfehler, der zu Falschberechnungen, Computer-Abstürzen, und dadurch letztlich auch zur Gefährdung von Menschenleben führt ich denke da zum Beispiel an Zugsteuerungen, das Bremssystem von Autos oder an medizinische Geräte." Die in seiner Forschergruppe entwickelten Verifikationsmethoden ermöglichen es, solche Korrektheitsaussagen oftmals auch für große industrielle Softwaresysteme vollautomatisch zu beweisen. So wird zum Beispiel das Passauer Verifikationssystem CPAchecker verwendet, um Teile von Computer-Betriebssystemen "auf Herz und Nieren" zu prüfen.

Katrina Jordan | 30.07.2014