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|
The Termination Problem Data Base (TPDB) is available as version 8. Programs are mainly available as source, and rewrite systems are represented in an XML-format. 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 CPF-format (version 2.1).
Please submit new problems for consideration in the TPDB to terminationcompetitionsc<at>lists.rwth-aachen.de with the subject prefixed by "[TPDB SUBMISSION]", before 12:01 CET on 27 May 2011.
The following categories will be featured in 2011:
- termination of conditional rewrite systems
- termination of context-sensitive 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 higher-order term rewrite systems
- termination of Java bytecode
- termination of logic programs
string rewrite systems
- certified relative termination
- certified termination
- relative termination
term rewrite systems
- certified relative termination
- certified termination
- innermost termination
- outermost termination
- relative termination
- termination of term rewrite systems modulo theories
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 problem-file 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 CPF-format. 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 TRS-file (in XTC-format) and the timeout in seconds. They should output YES / NO / MAYBE where in the first two cases a proof in CPF-format (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 XTC-format is the same as the one in the CPF-format 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 CPF-website.
Certifier can either be in one-pass or two-pass mode and this can be indicated when submitting a certifier.
In one-pass mode, it is assumed that there is one script which takes as input a CPF-file and the XTC-file in this order and terminates normally if the proof is accepted, and with some error-code 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 two-pass mode, there have to be two scripts. The first one takes as input a CPF-file and the XTC-file as before and produces some proof-script on standard-out if everything is fine or exits with some error-code which is interpreted as UNSUPPORTED. The second script is then invoked with the filename of the proof-script and should call the corresponding proof-assistent like Coq, Isabelle, ... It should again exit normally if the proof-script is accepted and with some error-code, otherwise, which is interpreted as REJECTED. Here, both the generated proof-script as well as the output of Coq, Isabelle, ... will be stored.
In two-pass 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 (m-n) seconds.
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.
ContactTo contact the steering committee of the termination competition, send email to terminationcompetitionsc<at>lists.rwth-aachen.de. The competition host can be reached at termcomp<at>informatik.uibk.ac.at.