Abstract:
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.