Program checking, program self-correcting and program self-testing
were pioneered by [Blum and Kannan] and [Blum, Luby and Rubinfeld] in
the mid eighties as a new way to gain confidence in software, by
considering program correctness on an input by input basis rather than
full program verification. Work in the field of program checking
focused on designing, for specific functions, checkers, testers and
correctors that are more efficient than the best program known for the
function. These were designed utilizing specific algebraic,
combinatorial or completeness properties of the function at hand.
In this work we introduce a novel composition methodology for
improving the efficiency of program checkers. We use this approach
to design a variety of program checkers that are provably more
efficient, in terms of circuit depth, than the {\em optimal} program
for computing the function being checked. Extensions of this
methodology for the cases of program testers and correctors are also
presented. In particular, we show:
\begin{itemize}
\item
For all $i\geq 1$, every language in $RNC^{i}$ (that is $NC^1$-hard
under $NC^0$-reductions) has a program checker in $RNC^{i-1}$.
In contrast to most previous work on program checking, these
checkers are for a {\em wide} class of functions {\em characterized
only by its complexity}, rather than by algebraic or combinatorial
properties. This characterization immediately yields new and
efficient checkers for languages such as graph connectivity, perfect
matching and bounded-degree graph isomorphism.
\item Constant-depth checkers, testers and correctors for the problems of matrix
multiplication, inversion, determinant and rank. Except for matrix multiplication, all
previous program checkers, testers and correctors for these problems run in nearly
logarithmic depth. Moreover, they all use the library notion of [Blum-Luby-Rubinfeld], in
which checkers have access to a library of programs for various matrix functions, rather
than only having access to a program for the function being checked.
\end{itemize}
Important ingredients in these results are new and very efficient
checkers for complete languages in low complexity classes (e.g.
$NC^1$). These constructions are based on techniques that were
developed in the field of cryptography.
