An 5 Tagen haben sich 36 ForscherInnen – trotz schönem Wetter – im Hörsaal zusammengefunden, um interessante Vorträge zu halten und zu hören, und um gemeinsam Ideen zu diskutieren, die dann zu weiteren Kooperationen führen können.
Im Folgenden werden die einzelnen Bestandteile von OSR kurz beschrieben.
ARI – Automation of Rewriting Infrastructure
Das ARI Projekt ist ein 3-jähriges gemeinschaftliches FWF-JSPS Projekt mit der CL-Gruppe als österreichischem Partner, sowie 4 japanischen Universitäten und Forschungszentren (Niigata University, Nagoya University, Japan Advanced Institute of Science and Technology, National Institute of Advanced Industrial Science and Technology). Es wird von Prof. Aart Middeldorp von der österreischen Seite und von Prof. Nao Hirokawa auf der japanischen Seite geleitet. Während des OSR fand ein 2-tägiges Treffen der ARI-Partner statt, um die angestrebten Ziele weiter zu verfolgen, d.h.:
- Entwicklung einer Infrastruktur, um internationale Wettbewerbe wie CoCo und termCOMP effizienter durchzuführen
- Ausbau der verifizierten Überprüfung von generierten Beweisen während dieser Wettbewerbe
- Erweiterung der Ausdrucksstärke von Termersetzungs-Systeme um logische Constraints, bei gleichzeitigem Ausbau der Analyse-Tools
Weitere Details zum Projekt sind auf der ARI Webseite verfügbar.
IWC und CoCo: Der Konfluenz-Workshop und die Konfluenz-Competition
Seit 2012 findet jährlich der Internationale Workshop on Confluence (IWC) statt, und 2023 wurde dieser unter Leitung von Cyrille Chenavier und Sarah Winkler als Teil von OSR organisert. Das Hauptthema ist die automatische Analyse von Konfluenz von Programmen, eine Eigenschaft die wichtig ist, um die Eindeutigkeit von Ergebnissen sicherzustellen, unabhängig davon, ob die Berechnungen sequentiell, parallel oder nicht-deterministisch ausgeführt werden.
Neben zwei eingeladenen Vorträgen von Naoki Nishida und René Thiemann war ein weiteres Highlight des IWC die 12. Confluence Competition (CoCo), der jährliche Wettbewerb unter Konfluenz-Analyse Tools. Trotz starker internationaler Konkurrenz konnten die CL-Tools in 5 von 12 Kategorien erste Preise gewinnen: CSI gewinnt in den Disziplinen NFP, SRS, TRS; CeTA siegt in der Certifier Kategorie; und FORT-h war das zuverlässigste Tool!
WST und termCOMP: Der Terminierungs-Workshop und die Terminierungs-Competition
Der internationale Workshop on Termination (WST) besteht seit 1993 und findet seitdem mindestens alle 2 Jahre statt. Dieses Jahr wurde er als Teil von OSR von Akihisa Yamada geleitet. Thematisch geht es seit jeher um die Frage, wie man – trotz Unentscheidbarkeit – für viele Programme automatisch die Terminierung nachweisen kann und deren Komplexität analysiert. Der eingeladene Vortrag von Benjamin Kaminski behandelte ein Thema, was in den letzten Jahren an Attraktivität gewonnen hat, nämlich die Terminierungs-Analyse von probabilistischen Programmen.
Auch beim WST fand parallel ein Wettbewerb statt, nämlich der internationale Wettbewerb der Terminierungs-Tools: termCOMP 2023. Bei diesem Wettbewerb konnte das CL-Tool TTT2 zwar in keiner Kategorie gewinnen, belegte aber immerhin einige 2. und 3. Plätze. In vielen Kategorien wurde zudem CeTA genutzt, um die automatisch generierten Terminierungsbeweise zu validieren. Dies war auch notwendig, da es dieses Jahr mehrere widersprüchliche Analysen der Tools gab.