CoCo 2016

News

September 8, 2016: Competition finished.
August 29, 2016: Added entrants.
August 19, 2016: Added detail of the execution platform.
July 26, 2016: Added detail of demostration categories.
March 20, 2016: 2nd CFP is announced.
March 19, 2016: Added detail of the registration.
March 17, 2016: The type of problems for the CTRS category is fixed to oriented CTRSs of type 3.
Jan 15, 2016: 1st CFP is announced.
Jan 7, 2016: This page is created

Results

Slides, details, details on StarExec, and results of CoCo 2016. Congratulations to the winners: CSI (TRS category), ConCon (CTRS category), CSI+CeTA/ConCon+CeTA (CPF category), and CSI^ho (HRS category).

Background

This site lists relevant information for the 5th Confluence Competition (CoCo 2016), collocated with CLA 2016 in Obergurgl, Austria. The competition will run live during the 5th International Workshop on Confluence (IWC 2016). We invite everyone developing confluence (and related) tools to join CoCo 2016, 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)

Furthermore, the following demonstration categories will be run:

• ground confluence of many-sorted term rewrite systems (GCR [R][A])
• unique normalization of term rewrite systems (UN) new!
• confluence of nominal rewrite systems (NRS)
• confluence of rewriting modulo theories of equational order-sorted conditional specifications (EOSCS-MT) new! (canceled)

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	February 28, 2016
request for demonstration categories	June 30, 2016
tool registration	August 21, 2016
tool submission	August 28, 2016, extended: August 30, 2016
problem submission	August 30, 2016, extended: September 1, 2016
competition	September 8, 2016

Database

These problems will be considered for CoCo 2016. Only problems of oriented CTRSs of type 3 are considered in the CTRS category. 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 2016 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 2016 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.

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=coco2016. 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)
URL of tool's website:                      (if there is one)

Please submit one page system description in EasyChair LaTeX class style highlighting the distinctive features of the prover (in a single latex file). System descriptions will be included in the proceedings of IWC 2016. Tool submission will be via StarExec. For the demonstration categories, the problem submission is via uploading the problem collection to StarExec together with the tool.

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
ACP	TRS/CPF	Takahito Aoto (Niigata University) Yoshihito Toyama (Tohoku University)	paper slides tools: ACP, ACP and CeTA
ACPH	HRS	Kouta Onozawa (Tohoku University) Kentaro Kikuchi (Tohoku University) Takahito Aoto (Niigata 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)	paper slides tools: ACP and CeTA, ConCon and CeTA, CSI and CeTA
CO3	CTRS	Naoki Nishida (Nagoya University) Takayuki Kuroda (Nagoya University) Karl Gmeiner (UAS Technikum Wien)	paper slides tool
CoLL-Saigawa	TRS	Nao Hirokawa (JAIST) Kiraku Shintani (JAIST)	paper slides tool
ConCon	CTRS/CPF	Thomas Sternagel (University of Innsbruck) Aart Middeldorp (University of Innsbruck)	paper slides tools: ConCon, ConCon and CeTA
CoScart	CTRS	Karl Gmeiner (UAS Technikum Wien)	paper tool
CRC	TRS/CTRS/Demo(EOSCS-MT)	Francisco Durán (University of Málaga)	paper (withdrawn)
CSI	TRS/CPF/Demo(UN)	Bertram Felgenhauer (University of Innsbruck) Aart Middeldorp (University of Innsbruck) Julian Nagele (University of Innsbruck)	paper slides tools: CSI, CSI and CeTA
CSI^ho	HRS	Julian Nagele (University of Innsbruck)	paper slides tool
FORT	Demo(UN)/Demo(GCR)	Franziska Rapp (University of Innsbruck) Aart Middeldorp (University of Innsbruck)	paper slides tool
Nrbox	Demo(NRS)	Takahito Aoto (Tohoku University) Kentaro Kikuchi (Tohoku University)	paper slides tool

Organising Committee

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