Starting in 2012, there is an annual international competition on confluence analysis (CoCo). Confluence is the property of some system, that if there are several ways to perform some computation steps, e.g. state 1 can lead to both state 2 and to state 3, then these computations can later on be joined again, i.e., the computation of both state 2 and state 3 can be continued to reach the same state 4. So, if a system is confluent, we know that evaluation strategies or other forms of non-determinism do not have any impact on the result.
During CoCo, several competing tools try to automatically prove or disprove confluence and related properties for as many systems as possible. Note that confluence is an undecidable property. Therefore, both resource limits as well as theoretical limits make this task challenging and interesting.
In this year CoCo 2024 was conducted in Tallinn during the international workshop on confluence. Overall, 12 tools participated in CoCo 2024, and they competed in 11 + 2 categories. Here, the 11 categories cover various flavours of confluence problems, e.g., by slightly changing the property or by changing the formalism of the input systems. The other 2 categories are about reliability of the generated proofs and disproofs.
After running all tools on the various confluence problems, one could see a remarkable performance of the confluence tools of the computational logic group: from the 13 categories, 8 categories have been won by the CL-tools (CSI (5x), CeTA (1x), crest (1x), and FORT-h (1x)). The other gold medals go to tools from Spain (3x) and Japan (2x).