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:
- 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