August 19, 2015: Confluence Competition 2015

The 4th Confluence Competition (CoCo 2015) is over. Three confluence tools and one certifier that are developed at CL participated and won several categories (results).

Confluence is one of the central properties of programs since it ensures uniqueness of computation results. Numerous results have been obtained on proving confluence of rewrite systems, lambda calculi, etc. and recently, several automatic tools for (dis)proving confluence have been developed. CoCo aims to foster the development of techniques for (dis)proving confluence automatically by setting up a dedicated competition among confluence tools.

CoCo 2015 was collocated with CADE-25 and ran live during the International Workshop on Confluence (IWC 2015) in Berlin. Previous editions of the competition were held in Nagoya (2012), Eindhoven (2013) and Vienna (2014).

In 2015 there have been four competition categories:

• confluence of first-order term rewrite systems (TRS)
• confluence of conditional term rewrite systems (CTRS)
• certification (CPF)
• confluence of higher-order term rewrite systems (HRS)

and tools from Innsbruck participated and won in all of them:

• CSI won the TRS category (draw with ACP)
• ConCon was the most powerful tool for CTRSs
• The certifier CeTA in combination with CSI won the category for certified confluence proofs
• CSI^ho was the strongest tool in the higher-order category

All these tools are open source.