The termination competition.pdf

The Termination Competition 2006 Claude Marche?1 and Hans Zantema2 1 LRI, Universite? Paris-sud 11 F-91405 ORSAY Cedex, France Claude.Marche@lri.fr 2 Department of Computer Science, Technische Universiteit Eindhoven P.O. Box 513, 5600 MB, Eindhoven, The Netherlands h.zantema@tue.nl Abstract. The third Termination Competition took place in June 2006. We present the background, results and conclusions of this competition. 1 Motivation and history In the past decades several techniques have been developed to prove termination of programs and rewrite systems. In the late nineties the emphasis in this research shifted towards automation: for a new tech- nique the final goal was not to use it by hand in order to prove termi- nation of a number of systems, but to implement it in such a way that termination proofs could be found fully automatically using a com- puter. Since around 2000 several tools were developed for this goal. In 2003 the idea came up to organize a competition on these tool by developing an extensive set of termination problems called TPDB (ter- mination problem data base), and run the tools on them and compare the results. The main objectives for such a competition were and are: ? stimulate research in this area, shifting emphasis towards automa- tion, and ? provide a standard to compare termination techniques. At the Workshop on Termination in 2003 in Valencia a preliminary competition was organized by Albert Rubio, together with the initial development of TPDB. Stimulated by the enthusiasm of the partici- pants it was decided to organize an annual competition, in which all tools run on one central computer and results are reported on-line. Claude Marche? took care of the organization and the development of the required tools. All details on the termination competition including past editions, rules and all results, are found on http://www.lri.fr/～marche/termination-competition/ The first full competition in this style run in May 2004, the week before t