Competition 2006 of termination tools

C. Marché and H. Zantema

March 10, 2006

1 Overview of the event

In June 2006, the third termination competition will be run.

The competition will be a completely automatic process that will be run without user interaction. During this competition, a large set of termination problems : the termination problem database (TPDB), will be considered, and each of these problems will be submitted to each tool willing to participate. An extra set of problems, called the secret problems, submitted by participants together with their tools, will also be considered.

Given a termination problem, each tool is supposed to answer whether the given system/program is terminating. Each tool must run without any user interaction.

The precise rules of the competition are detailed in the next section. Those who are willing to participate should register to the mailing dedicated to the competition, by sending a mail at

termtools-request@serveur-listes.lri.fr

with

subscribe termtools

in the body of the message.

2 Rules of the competition

A tool participating to the competition will be evaluated by a completely automatic process. There will be three categories: term rewrite systems, string rewrite systems, and logic programs. A tool may participate to any number of categories.

The tool must be available as an executable that takes as argument the name of a file describing a termination problem, and an integer giving the maximal CPU time in seconds allowed to give an answer. The tool is of course free to ignore this second information. The tool must run without any user interaction, and the answer must finally be printed on standard output. The tool may print anything on standard error, such as information on the differents attempts made.

For the term or string rewrite system category, the input file will be in the common format of the TPDB, available as a separate document. The answer must start by either YES or NO, meaning that the given rewrite system is terminating (respectively, not terminating) under the STRATEGY given in the input file. If there is no strategy annotation, strong termination is taken as the default. This text YES or NO should be followed by a proof trace of the claimed result : some text providing enough information for the termination being checked by a third party. Termination criteria involved must be clearly stated, with reference to relevant published paper. This proof trace must be in English or in the formal language of some proof assistants like ACL2, Coq, Isabelle/HOL, PVS.

Any output not starting by YES or NO is considered as DON'T KNOW. If a tool is still running when this maximal CPU time is reached, its process will be killed.

For the logic program category, the input file will be a Prolog program in a standard syntax as in the TPDB. Additionally, in the command line will be given an input query, of the form id(x₁,...,x_n) where each x_i is either i or o. The tool should answer whether the given program terminates on every query with that moding.

If it appears that for some termination problem a wrong answer is given, then the tool will be ``disqualified''.

In the competition every tool is applied on every system in TPDB in the corresponding categories, each with a time-out of 1 minute. After completing this first round, a second round is done in which every tool is applied on every system in TPDB in the corresponding categories for which no tool gave a YES or NO answer in the first round, each with a time-out of 5 minutes.

On the web page a score table will be presented for each category, by giving one point for each (correct) answer. Classifications will be computed for each category, several classifications will be made in the rewriting categories, with respect to strategies. The CPU time used will also be listed in the score table; the generated proofs or proof sketches will be accessible from the web page. There is nothing to win, except of being declared as ``the best automatic termination prover in the world in 2006'' in the given category. The main results of the competition will be reported at the Eighth International Workshop on Termination (WST 2006), August 15-16, 2006, in Seattle, USA.

3 The set of termination problems

The set of termination problems will be the termination problem database (TPDB) as it is on March 14, 2005. Any one may submit new termination problems for this database until May 11, 2006.

In order to make the competition more exciting, the set of termination problems used for the competition is extended by a secret list. This secret list is composed from systems that are submitted by the participants just before the competition. More precisely,

the deadline for submitting new publicly available termination problems for the data base is May 1,
the deadline for registration and submitting running versions of the tools is May 21,
the deadline for submitting the final versions of the tools is May 31,
the deadline for submitting termination problems for the secret list is May 31, and
the competition will start on Monday, June 5.

Every participant may submit at most 10 termination problems for the secret list for every category he participates. Typically, he may try to choose problems that can be solved by his tool while they are expected not to be solvable by the other tools.

4 Technical details for participants

If you are willing to participate to the competition, here is what you have to do in details:

One the authors of the tool (aka the corresponding author) must send a mail to Claude Marché (Claude.Marche at lri.fr) giving the following informations :
1. name of the tool
2. URL of the web page of the tool
3. author(s)
4. short description of the tool features (20 lines max)
One or more of the authors must register to the termtools mailing list as described above
As soon as possible, send the program itself, in a mail attachment or via an URL. The preferred form is directly a stand-alone executable for i386/Linux, since the evaluation will be performed on this architecture. If it is not possible for you to provide this, discuss with Claude.Marche at lri.fr to decide what to do.

The program must follow this specification:

The program which has to be run has to be called runme. It could be a shell script which runs the actual tool.
It runs without user interaction, only in "batch" mode writing on its standard output and standard error.
It takes as command line arguments the file name containing the termination problem to solve, a maximum allowed CPU time (an integer, in seconds), and for logic programs, an input query.
The answer must be given on the first line of the standard output, which must be either "YES" if termination has been established, or "NO" if non-termination has been established. Any other first line of answer is considered as "DON'T KNOW". The remaining lines of answer are required to be a proof trace as presented above. The full answer will be accessible from the result table. The standard error may be used to provide information on the attempts made by the tool, it will be also available from the results table.

Making the first of answer be "YES" or "NO" can of course be done by the runme script.
The program may create temporary files, but only in its current directory, and they must be erased after execution.

This document was translated from L^AT_EX by H^EV^EA.