\overlays{3}{
\begin{slide}{Certified Termination}

motivation: why do we believe the answers?
\begin{itemize}
\item SMT: 
  sat $\to$ print model, unsat $\to$ ??
\item Termination:
  no $\to$ print loop, yes $\to$ ??
\end{itemize}

solution: replace ``??'' by a formal proof,

and use mechanized proof checker.

approaches/implementations:
\begin{itemize}\itemsep 2pt
\item A3PAT (Coccinelle)/Coq
\item CoLoR/Coq
\item \fromSlide{2}{Isafor/Isabelle}
\item \fromSlide{3}{extraction (Isafor $\to$ Haskell)}
\end{itemize}
\end{slide}
}

\begin{slide}{Certified Termination (Results)}

term rewriting:

\begin{tabular}{lr}
total & 1391 problems \\
AProVE/CoLoR & 558 \\
AProve/CoLoR$\vee$A3PAT & 520 \\
Cime3/A3PAT & 485 
\end{tabular}

string rewriting:
\begin{tabular}{lr}
total & 732 problems \\
Matchbox/CoLoR & 466 \\
AProVE/CoLoR & 406 \\
AProve/CoLoR$\vee$A3PAT & 371
\end{tabular}


\end{slide}
