# 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:
- for any program P, it halts on all inputs of pi
- if P(x)=pi(x), for any x => C(pi, P, I, k) = CORRECT with probability >= 1 - 1/2^k
- if P(I)<>pi(I) => C(pi, P, I, k) = BUGGY with probability >= 1 - 1/2^k

## Problems that can be checked by a checker

- graph isomorphism
- equivalence search and canonical element problems
- group intersection problem
- factorization search problem