Confluence Competition

CoCo 2014


Jul 13, 2014: CoCo 2014 is over.
Jul 10, 2014: Problems have been selected
Jul 04, 2014: 7 tools have been submitted
Jun 28, 2014: Added entrants
Jun 17, 2014: Information about timeout
Apr 16, 2014: New category announced


Slides, details, and results of CoCo 2014. Slides at VSL Joint Award Ceremony.
Congratulations to the winners: ACP (TRS category), ConCon (CTRS category), and CeTA (CPF category).


This site lists relevant information for the 3rd Confluence Competition (CoCo 2014). The competition will run live during the 3rd International Workshop on Confluence (IWC 2014) in Vienna, Austria as part of the FLoC'14 Olympic Games. We invite everyone developing confluence (and related) tools to join CoCo 2014, to share problems and challenges.


The following categories will be run:


request for new categoriesMarch 7, 2014
tool registrationJune 27, 2014
tool submissionJuly 4, 2014
problem submissionJuly 9, 2014
competitionJuly 13, 2014
award ceremonyJuly 17, 2014


These problems will be considered for CoCo 2014. Submissions of new confluence problems are welcome. Submissions are via Cops. Problems submitted after the problem submission deadline will not be considered for the competition.

Execution Platform

CoCo 2014 will run on StarExec, a high-end cross-community competition platform. The 64-bit operating system will be Red Hat Enterprise Linux Workstation. Details of the specification are available here. CoCo 2014 will use nodes 0 - 32. For each problem a tool will have 60 seconds access to a single node (consisting of a quad-core Intel(R) Xeon(R) processors E5-2609 0 running at a clock rate of 2.40 GHz and 128 GB of main memory).


Tools must be able to run on the designated execution platform and read problems as input. The output of the tools must contain an answer in the first line followed by some proof argument understandable for human experts. Valid answers are YES (the input is confluent) and NO (the input is not confluent). Every other answer is interpreted as the tool could not determine the status of the input.

Every problem in the CTRS category is classified by the pair of

A tool should output UNSUPPORTED in place of YES/NO for input CTRSs in classes that the tool does not support.
For the certification category all tools capable of producing CPF output are first run on Cops. Then the successful proofs are considered for the certifiers.

It is encouraged that tools are open source and that binaries of the competition versions of the tools can be archived on the competition website.


Tool registration is via the contact email address. Please send us the following information: 1) tool name, 2) tool authors, 3) categories to enter (and for the CTRS category, unsupported classes if there are some), 4) contact mail address, and 5) URL of tool's website (if there is one). Every tool registration should also contain a one page system description (in PDF) highlighting the distinctive features of the prover. Tool submission is via StarExec.


The score is computed in percent of solved vs. supported problems (i.e. number of YES/NO answers vs. total – number of UNSUPPORTED answers). In case of a draw there might be more winners. The tool with the maximal score wins. An answer is plausible if it was not falsified (automatically or manually). A tool with at least one non-plausible answer cannot be a winner.


ACP confluence of TRS Takahito Aoto (Tohoku University)
Yoshihito Toyama (Tohoku University)
paper slides tool
CeTA certification Julian Nagele (University of Innsbruck)
René Thiemann (University of Innsbruck)
Harald Zankl (University of Innsbruck)
paper slides tool
CO3 confluence of CTRS (oriented, type 1) Naoki Nishida (Nagoya University)
Makishi Yanagisawa (Nagoya University)
Karl Gmeiner (UAS Technikum Wien)
paper slides tool
CoLL confluence of TRS Kiraku Shintani (JAIST) paper slides tool
ConCon confluence of CTRS (oriented, types 1-4) Thomas Sternagel (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tool
CSI confluence of TRS Harald Zankl (University of Innsbruck)
Bertram Felgenhauer (University of Innsbruck)
Aart Middeldorp (University of Innsbruck)
paper slides tool
Saigawa confluence of TRS Nao Hirokawa (JAIST)
paper slides tool

Organising Committee