Termination Competition
Deadlines for 2011 Competition
Competition start:  30 May 2011,  9:00 CEST (9am in Belgrad) 
Tool submission:  27 May 2011,  13:01 CEST 
Problem submission:  27 May 2011,  13:01 CEST 
Software requests:  13 May 2011,  13:01 CEST 
TPDB
The Termination Problem Data Base (TPDB) is available as version 8. Programs are mainly available as source, and rewrite systems are represented in an XMLformat. A converter is available to transform rewrite systems in the old format to the new XML format. Usage:
java jar convert.jar someTrs.trs > someTrs.xmlFor the other direction, the following converter can be used. It is invoked as follows:
xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trsThis requires that xsltproc is installed. The latter converter can be used by termination tools that do not accept the new XML format.
There also is an archive of example proofs where the aim is to certify these proofs (or detect that they are wrong). This archive consists of all generated proofs from the termination competition 2010 that validate against the schema. All proofs are given in the CPFformat (version 2.1).
New Problems
Please submit new problems for consideration in the TPDB to terminationcompetitionsc<at>lists.rwthaachen.de with the subject prefixed by "[TPDB SUBMISSION]", before 12:01 CET on 27 May 2011.
Competition Categories
The following categories will be featured in 2011:
 termination of conditional rewrite systems
 termination of contextsensitive rewrite systems

complexity of term rewrite systems
 derivational complexity for full rewriting
 derivational complexity for innermost rewriting
 runtime complexity for full rewriting
 runtime complexity for innermost rewriting
 termination of Haskell programs
 termination of higherorder term rewrite systems
 termination of Java bytecode
 termination of logic programs

string rewrite systems
 certified relative termination
 certified termination
 relative termination
 termination

term rewrite systems
 certified relative termination
 certified termination
 innermost termination
 outermost termination
 relative termination
 termination
 termination of term rewrite systems modulo theories
Competition Procedure
All participants on the same category will be run on a subset of the existing problems of this category. The number of problems is not fixed and will depend on the number of existing problems. The selection algorithm is described below. The running time for each problem is 60 seconds.
For nearly all categories, the tools will be started in their directory and obtain two parameters, first the problemfile and second, the timeout in seconds. The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML or CPFformat. Exceptions to these rules are listed below (e.g., other answers for certifiers and complexity tools, query for logic programs).
Although string rewriting problems will be considered as a particular case of the term rewrite systems in the TPDB, the string rewrite category will stay in the termination competition.
The certified categories will be run as follows:
 After the corresponding uncertified category of the competition has finished, the problems that have been solved (yes or no) are collected and form the initial selection for the certified category.
 Termination tools that can produce output in the new format and that participate in the certified competition are then run on the collection of 1, resulting in a collection of termination proofs. (Termination provers may use a different strategy from the uncertified competition, to increase chances of the proof being certified.)
 The certifiers are then run on the collection produced by 2.
The more detailed technical description for the certified competition is as follows.

Termination tools should provide a script which gets as only arguments the name of the TRSfile (in XTCformat) and the timeout in seconds. They should output YES / NO / MAYBE where in the first two cases a proof in CPFformat (version 2.1) has to be printed afterwards. Whereas the general format of CPF 2.1 has already been fixed, last minute extensions are accepted until May 27 as long as they are conservative, i.e., do not conflict with existing elements. Every output that does not correspond to this format will be refused. (This is done via xmllint example_proof.xml huge noout schema cpf.xsd)
To ensure that a (non)termination proof for the right TRS is given, afterwards one of the scripts checkEqualityYes/No.sh are called which are only successful if the TRS in the XTCformat is the same as the one in the CPFformat and if the proof goal corresponds to the YES / NO answer. Note, that for the equality testing no permutation of rules or renaming of variables is allowed. Both scripts are available for testing from the CPFwebsite.

Certifier can either be in onepass or twopass mode and this can be indicated when submitting a certifier.
In onepass mode, it is assumed that there is one script which takes as input a CPFfile and the XTCfile in this order and terminates normally if the proof is accepted, and with some errorcode if it is not accepted. In contrast to the 2010 competition, if the certifier does not accept, it should start its output with UNSUPPORTED or REJECTED on stdout, to differentiate between both outcomes.
In twopass mode, there have to be two scripts. The first one takes as input a CPFfile and the XTCfile as before and produces some proofscript on standardout if everything is fine or exits with some errorcode which is interpreted as UNSUPPORTED. The second script is then invoked with the filename of the proofscript and should call the corresponding proofassistent like Coq, Isabelle, ... It should again exit normally if the proofscript is accepted and with some errorcode, otherwise, which is interpreted as REJECTED. Here, both the generated proofscript as well as the output of Coq, Isabelle, ... will be stored.
In twopass mode the corresponding times are accumulated. For example, if the first script takes n seconds and there is a global timeout of m seconds, then the second script will be aborted after (mn) seconds.
Selection Algorithm
We will fix some number "c" with 0 < c < 1. This number indicates the percentage of problems to be taken from each family. So in principle, we would like to choose c * F problems from each family F. Here, F is the number of problems in the family F.
In order to avoid problems with very large or very small families, there will be two additional numbers "a" and "b" with 0 < a < b. Here, "a" is the minimum number of examples that should be chosen from each family. Similarly, "b" is the maximum number of examples that should be chosen from each family.
To illustrate this, let c = 1/2 and let a = 10 and b = 100. Then for a family F with 50 problems, we would randomly choose c * F = 25 problems from the family F. For a family F with 16 problems, we would not choose c * F = 8 problems, because this number would be smaller than a = 10. Instead, we would choose a = 10 problems randomly. For a family with 300 problems, we would not choose c * F = 150 problems, because this number would be larger than b = 100. Instead, we would choose b = 100 problems randomly.
To summarize, for every family F, we randomly choose:
c * F problems, if a <= c*F <= b a problems, if c*F < a b problems, if b < c*F
This rule is applied to every family with the same numbers a,b,c.
The numbers "a", "b" and "c" have been
chosen as in the last year: (a = 10, b = 75, c = 0.3).
Use of External Software in Termination Tools.
 Standard tools (SAT/SMT solvers) will be installed by the host,
 The configuration of the host machine is available.
 Requests for changes in the configuration must be submitted two weeks in advance of the competition. (Submit to simon.bailey<at>uibk.ac.at with the subject prefixed by "[TC SOFTWARE]", before 12:01 CET on 13 May 2011.
Contact
To contact the steering committee of the termination competition, send email to terminationcompetitionsc<at>lists.rwthaachen.de. The competition host can be reached at termcomp<at>informatik.uibk.ac.at.