\section{Certification}\label{subsec:cert}\label{sec:cert}

In the certified categories of the termination competition 2008,
the termination proofs are expressed in a formal language
and checked by machine. All participants used {\sf Coq}
as the underlying proof checker,
and one of two libraries 
that contain formalized knowledge on rewriting and termination:
\begin{itemize}
\item {\sf CoLoR}  (Coq Library on Rewriting and termination) 
\begin{itemize}
    \item  developed at INRIA, France, and TU Eindhoven, Netherlands,
      by Frederic Blanqui and Adam Koprowski,
    \item  home page: \url{http://color.inria.fr/}
\end{itemize}
\item {\sf A3PAT} (Assister Automatiquement les Assistants 
  de Preuve avec des Traces) 
\begin{itemize}
    \item   developed at Cedric, INRIA Sophia-Antipolis, LaBRI, LRI-PCRI, France,
      by Xavier Urbain et al.
    \item  home page: \url{http://a3pat.ensiie.fr/}
  \end{itemize}
\end{itemize}
{\sf Matchbox} uses {\sf CoLoR}, 
{\sf Cime3} uses {\sf A3PAT},
and {\sf AProVE} submitted three versions:
one that use each library alone, and one running
these two in parallel.

Of the total 1391 termination problems for term rewriting,
{\sf AProVE/CoLoR} produced 558 certified proofs,
followed by  {\sf AProVE/mixed} with 520 
and {\sf Cime3/A3PAT} with 485.


Of the total 732 termination problems in string rewriting,
{\sf Matchbox/CoLoR} produced 466 certified proofs,
followed by {\sf AProVE/CoLoR} with 406
and {\sf AProVE/mixed} with 371.

Let us compare the results with the certified category of 
the previous competition.
The problems used there were a strict subset of this years'.

For term rewriting,
the percentage of solved (by the winner) problems goes up from 36 \% to 40 \%.

This increase is mainly due to the availability
of the certified arctic matrix method.

In string rewriting, certification was first applied in 2008.
The percentage of uncertified solutions in 2007 is 65 \%,
and this is nearly equal to  the percentage 
of certified solutions in 2008, namely 64 \%.

Let us now compare the number of certified and uncertified 
proofs (obtained by the respective winners) in 2008.
In term rewriting, the certified winner
got 56 \% of the number of the uncertified winner,
while in string rewriting, the corresponding ratio is 93 \%.

This indicates that a state-of-the-art termination prover
for term rewriting needs to rely on techniques
that are (not yet) formally certified ``half of the time'',
while in string rewriting, this is necessary only in much fewer cases.

Current developments in certified termination are
\begin{itemize}
\item to provide alternative certification libraries and back-ends
(e.g., using {\sf Isabelle}),
\item
to improve efficiency 
(e.g., by having the termination certificates checked
by a {\sf Haskell} or {\sf ML} program 
that is derived automatically from an {\sf Isabelle} or {\sf Coq} text),
\item
to make more methods available for the standard categories
(e.g., sharper dependency graph approximations for proving termination,
and certification of loops for proving non-termination),
\item
to extend certification to other competition categories
(e.g., relative termination).
\end{itemize}
The long-term goal is to have \emph{all} statements
produced by termination provers in any category
verified automatically.

We note that with the current execution platform,
the actual certification of termination proofs
has a serious shortcoming: the platform checks validity of a proof
but not that it proves the right theorem.
Indeed it happened that a prover was working on different rewriting 
systems than intended because of some trivial programming error
in the the input parser. 

It is difficult to handle such problems because
different termination provers do not even agree
on the formalization of the statements and theorems,
since they are using different libraries and proof checkers.
The {\sf Rainbow} project aims to solve this problem
by providing a common format for termination proofs
that is independent of the prover and of the verifier.
Currently, {\sf Rainbow} is used as a high-level interface
to the {\sf CoLoR} library.
