Published Articles >> Table of Contents >> Abstract

2004 International Conference on Dependable Systems and Networks (DSN'04)   p. 399
Does Your Result Checker Really Check?
Lan Guo, West Virginia University, Morgantown, WV
Supratik Mukhopadhyay, West Virginia University, Morgantown, WV
Bojan Cukic, West Virginia University, Morgantown, WV

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSN.2004.1311909
Send link to a friend

Abstract
A result checker is a program that checks the output of the computation of the observed program for correctness. Introduced originally by Blum, the result checking paradigm has provided a powerful platform assuring the reliability of software. However, constructing result checkers 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 commercial LEDA system for combinatorial and geometric computing. In one of our case studies, we detected a logical error in a result checker for a program computing max flow of a graph.
Back to Top Additional Information
Citation:  Lan Guo, Supratik Mukhopadhyay, Bojan Cukic, "Does Your Result Checker Really Check?," dsn, p. 399,  2004 International Conference on Dependable Systems and Networks (DSN'04),  2004