Designing Programs That Check Their Work

Manuel Blum, Sampath Kannan
Computer Science Division
University of California at Berkeley

Verification = writing formal proofs of correctness for programs.
Checking = verifying that a program gives the correct answer.
Testing = running a program with a set of sample inputs, hoping that it will also work for real inputs.

C(pi, P, I, k) = checker for program P and problem pi = a probabilistic oracle Turing machine that:

Problems that can be checked by a checker