A (De)constructive Approach to Program Checking

Program checking, program self-correcting and program selftesting 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 which 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 optimal program for computing the function being checked. Extensions of this methodology for the cases of program testers and correctors are also presen...

• Type: Journal
• Year: 2007
• Where: ECCC
• Authors: Shafi Goldwasser, Dan Gutfreund, Alexander Healy, Tali Kaufman, Guy N. Rothblum
• Keywords: ECCC 2007, NSF Grants, NSF Grants CCF-0514167, Program Checkers