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.