MIT Department of Electrical Engineering & Computer Science

DATE: Thursday, December 15, 1994
TIME: 3:30pm Building 34 Room 101
TITLE: Result-Checking: A Theory of Testing Meets a Test of Theory
SPEAKER: Professor Manuel Blum

Coding theory is concerned with creating good error detecting/correcting codes for communication. Result-checking/correcting is concerned with creating good error detection/correction for computation. The goal is to find ways to detect each time a program makes mistakes, and to automatically correct all such errors. I am especially interested in detecting/correcting errors due to programming faults (bugs) in software or hardware.

For example, suppose that a chip designed to do some computation, division say, were found to give one incorrect output for every 10^9 divisions (one error every 21 minutes) on a sequence of "random" inputs. The use of result-checking/correcting could square this error probability, reducing it to one in every 10^18 divides (one error every 400 centuries).

This talk defines "program result checkers" and suggests how to construct checkers for a variety of problems. It points out the importance of randomization in the design of checkers, and the close tie between checkers and "probabilistic interactive proofs". The idea of checking leads naturally to the design of correctors for programs that make errors. As an example of what is possible, I show how to convert a package of fast but faulty programs for matrix multiplication, inversion, determinant, and rank into a package that works correctly and fast on all inputs without exception. In conclusion, I hint at general techniques that have been found useful for constructing result-checkers/correctors.