CSAIL Publications and Digital Archive header
bullet Research Abstracts Home bullet CSAIL Digital Archive bullet Research Activities bullet CSAIL Home bullet

link to publications.csail.mit.edu link to www.csail.mit.edu horizontal line

 

Research Abstracts - 2007
horizontal line

horizontal line

vertical line
vertical line

Designing Efficient Program Checkers by Delegating Their Work

Shafi Goldwasser, Dan Gutfreund, Alexander Healy, Tali Kaufman & Guy N. Rothblum

Summary

Program checking, program self-correcting and program self-testing were pioneered by Blum and Kannan [1] and Blum, Luby and Rubinfeld [2] 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. The bulk of the work in the field of program checking focused on designing, for specific functions, checkers (self correctors and self testers) which are more efficient than the best program known for the function. This was done by exploiting particular algebraic or combinatorial properties of the function at hand.

This work puts forth a new composition theorem for program checkers. The composition theorem (and its extensions) provide new structural tools for building program checkers, testers, and correctors. The crux of the new idea is to make these objects more efficient by delegating some of their work to the (potentially faulty) program being checked, corrected or tested.

Background

Verifying the correctness of software is one of the most important, and unfortunately also one of the most difficult, tasks facing programmers. In the mid eighties, Blum and Kannan [1] took an alternative approach to software verification for dealing with buggy code, and introduced the idea of Result Checking. Rather than trying to verify the correctness of the program on every input, they considered the easier goal of checking correctness on specific inputs. This approach has proved feasible and yielded program checkers for some interesting classes of functions, most notably for finite field arithmetic operations, matrix operations, and certain graph and group operations. A program checker for a function f, is a procedure C that is given black-box access to a program P that allegedly computes f  (we denote by CP the checker C together with its oracle access to P). It is required that with high probability (1) for every input x, CP(x) either rejects the program P or outputs the correct value f(x), and (2) if P does compute f correctly, then CP(x) outputs f(x).

A program checker can be used to verify whether a program P is correct on an input, but it does not give a method for computing the correct answer if P is found to be faulty. To address this issue, Blum, Luby and Rubinfeld [2], introduced the concept of program tester-corrector pairs. A tester is a procedure given black-box access to a program P, whose goal is to to estimate the probability that P errs on a random input x. A corrector is a procedure given black-box access to a program P whose goal is to recover f(x) for every x when P is not too faulty (i.e. does not err too much on random inputs and would be accepted by a tester). Various tester-corrector pairs were presented in [2], primarily for mathematical functions such as integer multiplication, the mod function etc. (and for other functions in later works). While the notion of program checking arises naturally in practical settings, it also had a tremendous impact on the theory of computing. The concepts and techniques introduced for program checking were pivotal in the early study of characterizing the power of IP and PCPs, as well as the development of the area of property testing.

A multitude of issues emerge in the field of program checking:

1. Checker Efficiency vs. Program Efficiency. A natural question is: how efficient can a program checker be compared to the program it checks? From a practical point of view it is clear that we want to minimize the overhead required to make sure that the program is correct. From a theoretical point of view it is interesting to understand the relations between the complexity of computing and the complexity of checking. Indeed this is one of the focuses of our work. We show that for a wide class of languages, checking can be provably more efficient than computing (in terms of circuit depth).

2. Libraries: Are They Necessary? In [2] Blum et al. consider the problem of testing and correcting matrix functions such as multiplication, inverse, determinant and rank. They suggested a non-standard model in which the checker/tester/corrector can access (with unit cost) not only the program to be checked, but also a library of (possibly faulty) programs that allegedly compute other related functions. Within this extended model, they show how to test and correct programs for the above matrix functions. For example, their determinant checker uses access both to a program that allegedly computes matrix determinant as well as a program that allegedly computes matrix multiplication. It remained an open problem to construct testers and correctors for the matrix operations of [2] without the use of a library. In this work, we eliminate the need for matrix libraries, and for libraries in general (as long as they obey certain hierarchical conditions).

3. A Need for Structural Tools. The bulk of work in the program checking field (and in some strong sense the primary achievements) has been in the design of efficient checkers/self correcters/self testers for {specific} functions, exploiting either algebraic or combinatorial properties of the functions at hand. There is a lack of structural tools which could be used to construct checkers or to make general statements about their existence or complexity (one exception is Beigel's theorem, see [1]). One of the main contributions of our work is providing new tools for constructing efficient checkers which apply to problems that are not necessarily complete. We also show how to leverage checkers for complete-problems toward the design of checkers for other (not necessarily complete) problems.

Our Results

This work puts forth a new composition theorem for program checkers. The composition theorem (and its extensions) provide new structural tools for building program checkers, testers, and correctors. The crux of the new idea is to make these objects more efficient by delegating some of their work to the (potentially faulty) program being checked, corrected or tested.

We use the structural tools obtained to address a multitude of issues which emerge in the field of program checking, showing the existence of checkers that are provably more efficient than the programs being checked (in terms of circuit depth) for entire complexity classes, and presenting explicit checkers for specific functions.

1. We show that for all i ≥ 1, every language in RNCi that is NC1-hard under NC0-reductions has a program checker in RNCi-1.

This is the first time checkers are designed for a class characterized by its complexity rather than algebraic or combinatorial properties. Furthermore, in terms of circuit depth, this yields checkers that are provably more efficient than the optimal program for the language they check. Examples of languages for which we get new and provably more efficient checkers are perfect matching, graph connectivity and bounded-degree graph isomorphism.

2. We eliminate the need for libraries in order to show checkers, testers, and correctors for matrix multiplication, inversion, rank and determinant. Instead we show standard checkers, testers and correctors, which need only access the program for the function tested rather than an entire library. These checkers are provably more efficient than the optimal program for computing these functions in terms of circuit depth. Furthermore, we provide reasonable conditions under which general program libraries can be eliminated.

Finally, we show very efficient (either NC0 or AC0) checkers, correctors, and testers for several functions that are complete for various complexity classes (this include parity and the NC1-complete language introduced by Barrington). We use these as additional tools together with the main composition theorem, to prove the previously stated results.

Support

This research was supported by NSF grant, CNS-0430450, NSF grant CFF-0635297 and a Cymerman-Jakubskind award 

References:

[1]   Manuel Blum and Sampath Kannan.  Designing programs that check their work. Journal of the ACM 42(1): 269--291, 1995.

[2] Manuel Blum, Michael Luby and Ronitt Rubinfeld. Self-Testing/Correcting with Applications to Numerical Problems. Journal of Computer and System Sciences 47(3):549--595, 1993.

vertical line
vertical line
 
horizontal line

MIT logo Computer Science and Artificial Intelligence Laboratory (CSAIL)
The Stata Center, Building 32 - 32 Vassar Street - Cambridge, MA 02139 - USA
tel:+1-617-253-0073 - publications@csail.mit.edu