\section{Introduction} \label{sec:intro}

The \emph{Termination Competition} is 
an annual event to showcase and compare software 
that automatically proves termination of rewriting systems 
and logic and functional programs.

The goal of the competition is
to encourage research for new termination techniques, 
as well as efficient implementation and combination of known techniques;
and at the same time to show outside the community 
that automated termination provers
are mature, reliable and ready to be used in applications.

The precursor of the current termination competition
was an exhibition of termination provers, organized by Albert Rubio,
during the Workshop on Termination 2003 in Valencia.
There, the participants decided to make this a regular event,
using specific sets of termination problems,
a specific procedure for submitting provers
and running them on an execution platform,
as well as a unified presentation of results on the web.

Past termination competitions were run by 
Claude March\'{e} and Albert Rubio in 2004 \cite{termcomp04},
and by Claude March\'{e} and Hans Zantema in 2005, 2006, and 2007 
\cite{termcomp05,DBLP:conf/rta/MarcheZ07,termcomp07}.
Since 2008, the competition is hosted by the Computational
Logic Group at the University of Innsbruck.
The host provides a hardware and software platform
for the automated submission and execution of termination provers.
See Section~\ref{sec:plat} for technical detail.

A \emph{Termination problem data base} (TPDB) was established in 2003,
based on termination problems collected from publications
in the field,
and growing continually by submissions of new termination
problems, mostly by authors of termination provers,
but also from applications areas. 
E.g., TPDB contains most of the functions from the Haskell Prelude.
In Section \ref{sec:cat} we give some detail
on the semantics and current contents of TPDB.

The termination competition of 2008 was executed in three stages
at the end of the year (and beginning of the next year),
and this paper gives an account 
of the participants (in Section~\ref{sec:participants})
and results (following sections).
In particular we discuss
some recent developments:
2008
was the first competition that included 
automated investigations of derivational complexity
(see Section~\ref{sec:complex}),
and the second competition with (optional)
automated verification of termination proofs (see Section~\ref{sec:cert}).
We conclude with some comments on the future of the competition
in Section~\ref{sec:discussion}.

Strategic decisions for the competition and its future are made
by a steering committee, consisting of representatives
of the participating research groups.
Developers and users of automated termination provers
subscribe to the \verb|termtools| mailing list,
and there is a central information resource for the termination community
\url{http://termination-portal.org/}, 
hosted by Lehr- und Forschungsgebiet Informatik 2 of RWTH Aachen.

This report is based on contributions by
Simon Bailey (Platform), 
Frederic Blanqui (Certification),
Jürgen Giesl (LP/FP/SRS/TRS), 
and Georg Moser (Complexity).
The views expressed in Section~\ref{sec:discussion} are the editor's.
