CoCo 2014

News

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

Results

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).

Background

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.

Categories

The following categories will be run:

• confluence of first-order term rewrite systems
• confluence of conditional term rewrite systems new!
• certification

Timeline

request for new categories	March 7, 2014
tool registration	June 27, 2014
tool submission	July 4, 2014
problem submission	July 9, 2014
competition	July 13, 2014
award ceremony	July 17, 2014

Database

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

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 condition type (oriented, join, semi-equational), and
• a type of CTRS (type 1, 2, 3, or 4).

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.

Registration/Submission

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.

Scoring

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.

Entrants

tool	categories	authors	material
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

• Takahito Aoto (Tohoku University, Japan) chair
• Nao Hirokawa (JAIST, Japan)
• Harald Zankl (University of Innsbruck, Austria)