Logo der Universität Passau

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.

| Lesedauer: 2 Min.

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.

Kontakt

Referat für Medienarbeit

Rückfragen zu dieser Pressemitteilung richten Sie bitte an:

Nicola Jacobi und Barbara Weinert
Tel.: +49 851 509-1434, -1450
kommunikation@uni-passau.de

Ich bin damit einverstanden, dass beim Abspielen des Videos eine Verbindung zum Server von Vimeo hergestellt wird und dabei personenbezogenen Daten (z.B. Ihre IP-Adresse) übermittelt werden.
Ich bin damit einverstanden, dass beim Abspielen des Videos eine Verbindung zum Server von YouTube hergestellt wird und dabei personenbezogenen Daten (z.B. Ihre IP-Adresse) übermittelt werden.
Video anzeigen