CoCo 2015

News

Aug 2, 2015: Competition finished.
Jun 21, 2015: Added detail of the execution platform.
Jun 21, 2015: Added entrants.
Jun 20, 2015: Information about CPF category revised.
May 13, 2015: Tool registration method is updated and system description format is specified.
Jan 06, 2015: First HRSs added to Cops
Dec 10, 2014: Detail information is added
Dec 08, 2014: This page is created

Results

Slides, details, and results of CoCo 2015. A report at CADE-25.
The following answers turn out to be incorrect: Cops ♯455 by ACPH and Cops ♯262 by CoScart.
Congratulations to the winners: ACP and CSI (TRS category), ConCon (CTRS category), and CSI+CeTA (CPF category) and CSI^ho (HRS category).

Background

This site lists relevant information for the 4th Confluence Competition (CoCo 2015), collocated with CADE-25 in Berlin, Germany. The competition will run live during the 4th International Workshop on Confluence (IWC 2015). We invite everyone developing confluence (and related) tools to join CoCo 2015, to share problems and challenges.

Categories

The following categories will be run:

• 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) new!

Furthermore, the following demonstration categories will be run: new!

• ground confluence of many-sorted term rewrite systems (GCR)
• confluence of nominal rewrite systems (NRS)

Besides these categories, new categories will be considered if there are tools and problems dedicated to those categories. We welcome requests for categories. We solicit new categories for the competition (competition categories) as well as demonstration categories. Demonstration categories are one-time events for demonstrating new attempts and/or merit of particular tools, where a problem set need not to stem from Cops. For instance, the next categories are in the scope of demonstration: right-ground TRSs, CTRSs of specific condition type, eTRSs, ground confluence and the unique normal form property.

Timeline

request for competition categories	January 31, 2015
request for demonstration categories	May 31, 2015
tool registration	July 19, 2015
tool submission	July 26, 2015
problem submission	July 28, 2015
competition	August 2, 2015

Database

These problems will be considered for CoCo 2015. 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 2015 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 2015 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).

Request for Categories

Request for new categories is via the contact email address. Please send us the following information at your earliest convenience:

• category type (competition category or demonstration category)
• description of problems and semantics (rewrite steps, confluence, etc.) together with adequate references
• a proposal of the input format (if necessary)

It is preferable that a prototype of the tool and sample problems are available at the time of the request. Please note that for competition categories we presume integration of problem collections into our database for running the competition. Requests for categories may be rejected for technical reasons.

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 CPF category, each participant should output certifiable proofs as well as the result of certification: YES followed by a certifiable proof (e.g. a proof in cpf format) if confluence proof is certified, and NO followed by a certifiable proof if non-confluence proof is certified. A tool should output UNSUPPORTED in place of YES/NO for input (C)TRSs in classes that the tool does not support; in particular, a tool that is not registered to any TRS (CTRS) category should output UNSUPPORTED for any input of CTRSs (resp. TRSs).

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 must be made electronically through the EasyChair system at: https://www.easychair.org/conferences/?conf=coco2015. Specify tool name as the title and tool authors as the authors. Please use the following form for the abstract:

Categories to enter: TRS/CTRS/CPF/HRS/Demo  (leave appropriate ones)
(Un)supported classes for CTRS category:  (if there are)
Coupled tools for CPF category:           (if there are) 
URL of tool's website:                    (if there is one)

Please submit one page system description in EasyChair style highlighting the distinctive features of the prover (in a single latex file). System descriptions will be included in the proceedings of IWC 2015. 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	TRS/CPF	Takahito Aoto (Tohoku University) Yoshihito Toyama (Tohoku University)	paper slides tools: ACP, ACP and CeTA
ACPH	HRS	Kouta Onozawa (Tohoku University) Kentaro Kikuchi (Tohoku University) Takahito Aoto (Tohoku University) Yoshihito Toyama (Tohoku University)	paper slides tool
AGCP	Demo(GCR)	Takahito Aoto (Tohoku University) Yoshihito Toyama (Tohoku University)	paper slides tool
CeTA	CPF	Julian Nagele (University of Innsbruck) Christian Sternagel (University of Innsbruck) Thomas Sternagel (University of Innsbruck) René Thiemann (University of Innsbruck) Sarah Winkler (University of Innsbruck) Harald Zankl (University of Innsbruck)	paper slides tools: ACP and CeTA, ConCon and CeTA, CSI and CeTA
CO3	CTRS (oriented, type 1)	Naoki Nishida (Nagoya University) Takayuki Kuroda (Nagoya University) Makishi Yanagisawa (Nagoya University) Karl Gmeiner (UAS Technikum Wien)	paper slides tool
CoLL-Saigawa	TRS	Nao Hirokawa (JAIST) Kiraku Shintani (JAIST)	paper slides tool
ConCon	CTRS (oriented, types 1-4)/CPF	Thomas Sternagel (University of Innsbruck) Aart Middeldorp (University of Innsbruck)	paper slides tools: ConCon, ConCon and CeTA
CoScart	TRS/CTRS(oriented, type 1-3)	Karl Gmeiner (UAS Technikum Wien)	paper slides tool
CSI	TRS/CPF	Bertram Felgenhauer (University of Innsbruck) Aart Middeldorp (University of Innsbruck) Julian Nagele (University of Innsbruck) Harald Zankl (University of Innsbruck)	paper slides tools: CSI, CSI and CeTA
CSI^ho	HRS	Julian Nagele (University of Innsbruck)	paper slides tool
NoCo	Demo(NRS)	Takaki Suzuki (Tohoku University) Kentaro Kikuchi (Tohoku University) Takahito Aoto (Tohoku University)	paper slides tool

Organising Committee

• Takahito Aoto (Tohoku University, Japan) chair
• Nao Hirokawa (JAIST, Japan)
• Julian Nagele (University of Innsbruck, Austria)
• Naoki Nishida (Nagoya University, Japan)
• Harald Zankl (University of Innsbruck, Austria)