CoCo 2012
This site lists relevant information for the confluence competition 2012. The competition will take place as part of the 1st International Workshop on Confluence (IWC 2012), which is collocated with the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012). The competition will run during the workshop and results will be reported at RTA 2012.Results
ACP gained 96 points and came first while saigawa came second with 89 points just before CSI with 88 points. See details here. You can see slides of the report at RTA 2012.Registration/Submission
Registration and tool submission is via the contact email address. Please also consider to submit a one page (EasyChair style) system description of your tool via Easychair, which will be added to the proceedings of IWC 2012.Timeline
| registration | April 1 - May 15, 2012 |
| system description | April 15 - May 15, 2012 |
| tool submission (for testing) | May 1 - May 15, 2012 |
| final version of tool | May 22, 2012 |
| competition | May 29, 2012 |
Host
CoCo 2012 will be hosted on a server with 8 dual-core AMD Opteron processors 885 running at a clock rate of 2.6 GHz and 64 GB of main memory. The operating system is Linux CentOS release 5 (Final). Every tool is allowed 60 seconds for each problem.
Database
These problems will be considered for CoCo 2012.
Tools
We invite everyone to join CoCo. Tools must be able to read these 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.
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.
The host may reject tools that are not running on the designated hardware.
Scoring
Every tool gets one point for each plausible answer. An answer is plausible if it was not falsified (automatically or manually). The tool with the maximal score wins. In case of a draw there might be more winners. A tool with at least one non-plausible answer cannot be a winner.
Certification demo
Besides the main track, we will run a certification demo. In this demo, tools will try to certify (non)confluence proofs in CPF format. Certification tools are supposed to output 'YES' ('NO') if the certification of a (non)confluence proof succeeded. Certifiable proofs will be prepared prior to the competition.
Entrants
| tool | division | authors |
|---|---|---|
| ACP 0.31 | confluence tool | Takahito Aoto (Tohoku University) Yoshihito Toyama (Tohoku University) |
| CeTA 2.5 | certification tool | René Thiemann (University of Innsbruck) |
| CSI 0.2 | confluence tool | Harald Zankl (University of Innsbruck) Bertram Felgenhauer (University of Innsbruck) Aart Middeldorp (University of Innsbruck) |
| Saigawa 1.4 | confluence tool | Nao Hirokawa (JAIST) Dominik Klein (JAIST) |
Organising Committee
- Takahito Aoto (Tohoku University, Japan) chair
- Nao Hirokawa (JAIST, Japan)
- Harald Zankl (University of Innsbruck, Austria)