Does Your Result Checker Really Check?

A result checker is a program that checks the output of the computation of the observed program for correct-ness. Introduced originally by Blum, the result checking paradigm has provided a powerful platform assuring the reliability of software. However, constructing result check-ers for most problems requires not only significant domain knowledge but also ingenuity and can be error prone. In this paper we present our experience in validating result checkers using formal methods. We have conducted several case studies in validating result checkers from the commer-cial LEDA system for combinatorial and geometric comput-ing. In one of our case studies, we detected a logical error in a result checker for a program computing max flow of a graph. 1