Innsbrucker ForscherInnen holen drei Auszeichnungen bei den „Olympischen Spielen der Logik“

Der „Vienna Summer of Logic“ versammelte über 2500 LogikerInnen der Welt in Österreich. Im Rahmen dieser Veranstaltung wurden die ersten „FLoC Olympic Games“ abgehalten. Die Spiele umfassten 14 verschiedene Wettbewerbe auf vielfältigen Gebieten der Informatik rund um die bedeutsame Frage der Softwareverifikation mittels logischer Methoden und deren Implementierung in automatische Werkzeuge. Im Gesamten traten hunderte Beweiser und Teams gegeneinander an, um zu zeigen, wie gut heutzutage theoretische Resultate in hochkomplexe Softwarewerkzeuge integriert werden können, die in der Lage sind, vollautomatisch essentielle Eigenschaften ihrer Eingabe zu verifizieren. Je nach Disziplin war die Eingabe die logische Abstraktion eines Schaltkreises, konkreter Programmcode, oder logische Sätze. Entsprechend vielfältig waren die Aufgaben der verwandten Softwarewerkzeuge: das Auffinden von logischen Fehlern in Computerchips, das automatische Analysieren von Programmcode, das automatische Erstellen von mathematischen Beweisen.

Der Innsbrucker Computational-Logic-Gruppe gelang es, drei der begehrten Kurt-Gödel-Medaillen zu erobern. Die ForscherInnen nahmen mit neun Beweisern in drei verschiedenen Disziplinen teil und gewannen drei Medaillen. Mit diesem herausragendem Ergebnis knüpfen die Innsbrucker InformatikerInnen an ihre Erfolge an: erst kürzlich erhielt der Informatiker René Thiemann, Computational-Logic-Gruppe, den START-Preis, die höchstdotierte Förderung für hochbegabte junge ForscherInnen in Österreich.

„FLoC Olympic Games“

Mit der erstmaligen Austragung der „Olympischen Spielen der Logik“ in Wien wollen die Initiatoren eine neue wissenschaftliche Tradition begründen. Diese hochkarätigen Informatik-Wettbewerbe sollen zukünftig alle vier Jahre in dieser Form stattfinden. Verteilt über alle Wettbewerbe konnten insgesamt 43 der begehrten Auszeichnungen gewonnen werden, 13 Medaillen gingen an österreichische ForscherInnen.

PreisträgerInnen

• Martin Avanzini / Andreas Kochesser / Georg Moser / Michael Schaper / Maria Schett (Termination Competition, Kategorie: Complexity Analysis of Term Rewriting, Tool: TcT)
• Aart Middeldorp / Thomas Sternagel (Confluence Competition, Kategorie: Confluence of Conditional Term Rewrite Systems, Tool: ConCon)
• Julian Nagele / Rene Thiemann / Harald Zankl (Confluence Competition, Kategorie: Certification, Tool: CeTA)

(Georg Moser, Gabriele Strasser)