Program checking is a new approach to software fault-tolerance. For a program that computes a function, a checker tests whether the program's output is correct for a specific input. Even when the program makes mistakes, the checker uses the program itself to perform the test by applying the program to several inputs related to the original one. The checker provides a probabilistic guarantee of correctness on a particular input on which the program is executed, whereas formal program verification establishes correctness on all inputs prior to execution. In this project, traditional fault-tolerance techniques are combined with program checking to produce new kinds of program checkers that are effective for programs of practical size. In particular, program checking is combined with certification trails and with algorithm-based fault-tolerance, a technique for concurrent error detection. Further, program checking is applied to operating system algorithms that ensure the truth of predicates such as mutual exclusion, deadlock avoidance, and serializability of concurrent transactions.
