Certifying Algorithms
The I/O-behavior of a program is specified by a precondition $\phi(x)$ and a
postcondition
$\psi(x,y)$. On input $x$ satisfying $\phi$, the program is supposed to return a
$y$ such that $\psi(x,y)$. However, a user of a program has now way to know whether
$\psi(x,y)$ actually holds.
A certifying algorithm returns in addition a witness $w$ with the property
that knowledge of $x$, $y$, and $w$ makes it easy to verify that $\neg \phi(x)
\vee \psi(x,y)$.
We give a simple example, the task of deciding whether a graph is bipartite.
A certifying algorithm returns a two-coloring if the input graph is bipartite
and returns an odd cycle if the input graph is not bipartite.\smallskip
Certifying algorithms have many advantages over conventional algorithms. In
particular, they can be tested on {\bf every} input and not just on inputs for
which the result is known by other means, and they are reliable in the sense
that they either give the correct answer or raise an error. Most programs in
the LEDA library are certifying.
The design of certifying programs and certifying data stuctures
raises new algorithmic questions. We give a
survey of results:
\begin{itemize}
\item certifying graph algorithms
\item checking data structures
\item certifying geometric algorithms
\item the advantages of certifying algorithms.
\item can every algorithm be made certifying?
\end{itemize}