[Termination tools] announcement termination competition

H. Zantema hzantema at win.tue.nl
Mon Feb 7 17:50:46 CET 2005


Dear colleagues,

Claude Marche and me are preparing the termination competition for 
2005. Below you may find our proposal for the announcement. Comments
on this proposal can be sent to me until February 16, after which the
announcement will be distributed widely over the community.

As you may see a difference with last year's competition is that every
participant may submit a number of secret systems just before the start
of the competition (we think of at most 20 systems per participant).
For the rest the competition set will consist of a selection of the 
TPDB by that time, for which any one of you may submit new systems 
that will be added according reasonable guidelines (for instance, not 
1000 automatically generated systems), and that will be made public
in advance. We think of selecting either all systems, only filtering
out duplicates, or also filter out systems that were solved last year
by all or most of the systems. In case we agree about the protocol on
the termtools list, and we do not receive the secret systems before the
deadline of the final version of the tools, as participants we two do not 
have any advantage of being organizers too.

 From the minutes of our meeting in Aachen I recall:

* For all participating tools the executable should be freely available.

* There should be a fixed time limit for each termination problem. It
  is proposed to define it to be one minute. 

* It is mandatory that not only `YES' or `NO' is generated as the output,
  but also a proof (outline).

The homepage of the termination competition will be adjusted to contain
these rules, the deadlines, and so on.

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+



After the success in 2003 in Valencia and in Aachen in 2004 also this 
year again there will be a 
 
	TERMINATION COMPETITION

Every one who has developed or is developing a tool for automatic 
proving termination is invited to participate.

There will be at least three categories:

	term rewriting, string rewriting and logic programming.

People that want to participate in another category are asked to 
contact us. 

The competition will consist of a completely automatic process that will 
be run without user interaction, starting on Monday April 11, 9:00 GMT.
Results will be reported run-time on the web. Apart from that at the RTA 
conference in Nara, Japan, April 19-21, a slot in the schedule will be 
reserved for presenting results. During the competition, a large set of
termination problems, extracted from the public termination problem database 
(TPDB) and a secret list of problems, will be considered, and each of 
these problems will be submitted to each participating tool. In every 
category the winner is the tool generating the highest number of proofs
of termination or non-termination. The secret list is composed from
systems that are submitted by the participants just before the competition.

The main objective of this competition is the encouragement of research in 
the area of automatic generation of termination proofs. Last years this
has been very succesfull.  In order to continue this success we prefer
all tools in this area to participate, including tools on prototyping
level and tools only applying a single technique. We want to stress that
not only the ultimate winners are succesfull, but all tools that can 
generate a proof for any system for which other tools fail. In this way 
also tools only applying a single technique may be successful, and may 
provide a stimulus for other tools to include this technique too.

In order to keep the competition challenging it is important that new
systems are added to the database. Every one is invited to propose new
systems. 

Participants should submit (the first versions of) their tools not later
than March 21. Details of how to submit and details of the rules, and
results of last year can be found on

http://www.lri.fr/~marche/wst2004-competition/


		Claude Marche (Claude.Marche at lri.fr)
		Hans Zantema (h.zantema at tue.nl)



More information about the Termtools mailing list