Over 5 days, 36 researchers came together in the lecture theatre - despite the fine weather - to give and listen to interesting presentations and to discuss ideas together that could then lead to further collaborations.
The individual components of OSR are briefly described below.
ARI - Automation of Rewriting Infrastructure
The ARI Project is a 3-year joint FWF-JSPS project with the CL Group as the Austrian partner, as well as 4 Japanese universities and research centres (Niigata University, Nagoya University, Japan Advanced Institute of Science and Technology, National Institute of Advanced Industrial Science and Technology). It is led by Prof Aart Middeldorp on the Austrian side and Prof Nao Hirokawa on the Japanese side. During the OSR, a 2-day meeting of the ARI partners took place to further pursue the desired goals, i.e:
- Developing an infrastructure to organise international competitions such as CoCo and termCOMP more efficiently
- Expansion of the verified review of generated evidence during these competitions
- Extending the expressive power of term substitution systems to include logical constraints, while at the same time expanding the analysis tools
Further details on the project are available at ARI website
IWC and CoCo: The Confluence Workshop and the Confluence Competition
The International Workshop on Confluence (IWC) has been held annually since 2012, and in 2023 it was organised under the leadership of Cyrille Chenavier and Sarah Winkler as part of OSR. The main topic is the automatic analysis of confluence of programmes, a property that is important to ensure the uniqueness of results, regardless of whether the computations are executed sequentially, in parallel or non-deterministically.
In addition to two invited talks by Naoki Nishida and René Thiemann, another highlight of the IWC was the 12th Confluence Competition (CoCo), the annual competition among confluence analysis tools. Despite strong international competition, the CL tools won first prizes in 5 out of 12 categories: CSI won in the NFP, SRS, TRS disciplines; CeTA won in the Certifier category; and FORT-h was the most reliable tool!
WST and termCOMP: The scheduling workshop and the scheduling competition
The international Workshop on Termination (WST) has existed since 1993 and has taken place at least every 2 years since then. This year it was chaired by Akihisa Yamada as part of OSR. The topic has always been the question of how to automatically prove the scheduling of many programs and analyse their complexity - despite undecidability. The invited lecture by Benjamin Kaminski dealt with a topic that has become increasingly attractive in recent years, namely the scheduling analysis of probabilistic programmes.
A competition also took place in parallel at the WST, namely the international competition of scheduling tools: termCOMP 2023. Although the CL tool TTT2 did not win any of the categories in this competition, it did take 2nd and 3rd place. In many categories, CeTA was also used to validate the automatically generated scheduling proofs. This was also necessary as there were several contradictory analyses of the tools this year.