loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2004 International Conference on Dependable Systems and Networks (DSN'04)
Does Your Result Checker Really Check?
Florence, Italy
June 28-July 01
ISBN: 0-7695-2052-9
Lan Guo, West Virginia University, Morgantown, WV
Supratik Mukhopadhyay, West Virginia University, Morgantown, WV
Bojan Cukic, West Virginia University, Morgantown, WV
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.
Citation:
Lan Guo, Supratik Mukhopadhyay, Bojan Cukic, "Does Your Result Checker Really Check?," dsn, pp.399, 2004 International Conference on Dependable Systems and Networks (DSN'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.