Designing Programs That Check Their Work

Manuel Blum, Sampath Kannan
Computer Science Division
University of California at Berkeley
http://citeseer.nj.nec.com/blum89designing.html

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