Seit 2012 findet jährlich ein internationaler Wettbewerb zur Konfluenzanalyse (CoCo) statt. Konfluenz ist die Eigenschaft eines Systems, dass, wenn es mehrere Möglichkeiten gibt, bestimmte Berechnungsschritte auszuführen, z. B. Zustand 1 sowohl zu Zustand 2 als auch zu Zustand 3 führen kann, diese Berechnungen später wieder verbunden werden können, d. h. die Berechnung von Zustand 2 und Zustand 3 kann fortgesetzt werden, um denselben Zustand 4 zu erreichen. Wenn ein System also konfluent ist, wissen wir, dass Bewertungsstrategien oder andere Formen des Nicht-Determinismus keinen Einfluss auf das Ergebnis haben.
Während CoCo versuchen mehrere konkurrierende Werkzeuge, Konfluenz und verwandte Eigenschaften für so viele Systeme wie möglich automatisch zu beweisen oder zu widerlegen. Beachten Sie, dass Konfluenz eine unentscheidbare Eigenschaft ist. Daher ist diese Aufgabe sowohl aufgrund der begrenzten Ressourcen als auch der theoretischen Grenzen eine Herausforderung und interessant.
In diesem Jahr wurde CoCo 2024 in Tallinn während des internationalen Workshops über Konfluenz durchgeführt. Insgesamt nahmen 12 Tools an der CoCo 2024 teil, die in 11 + 2 Kategorien gegeneinander antraten. Die 11 Kategorien decken verschiedene Arten von Konfluenzproblemen ab, z.B. durch leichte Änderung der Eigenschaft oder durch Änderung des Formalismus der Eingabesysteme. In den anderen 2 Kategorien geht es um die Zuverlässigkeit der erzeugten Beweise und Widerlegungen.
Nachdem alle Tools auf die verschiedenen Konfluenzprobleme angewendet wurden, konnte man eine bemerkenswerte Leistung der Confluence Tools der Computational Logic Group feststellen: von den 13 Kategorien wurden 8 Kategorien von den CL-Tools gewonnen (CSI (5x), CeTA (1x), crest (1x) und FORT-h (1x)). Die anderen Goldmedaillen gehen an Tools aus Spanien (3x) und Japan (2x).
