Error explanation with distance metrics |
| |
Authors: | Alex Groce Sagar Chaki Daniel Kroening Ofer Strichman |
| |
Affiliation: | (1) Chaki JPL Laboratory for Reliable Software California Institute of Technology, 4800 Oak Grove Drive Pasadena, CA, 91009;(2) ETH Zurich, Zurich, Switzerland;(3) Technion, Haifa, Israel |
| |
Abstract: | In the event that a system does not satisfy a specification, a model checker will typically automatically produce a counterexample
trace that shows a particular instance of the undesirable behavior. Unfortunately, the important steps that follow the discovery
of a counterexample are generally not automated. The user must first decide if the counterexample shows genuinely erroneous
behavior or is an artifact of improper specification or abstraction. In the event that the error is real, there remains the
difficult task of understanding the error well enough to isolate and modify the faulty aspects of the system. This paper describes
a (semi-)automated approach for assisting users in understanding and isolating errors in ANSI C programs. The approach, derived
from Lewis’ counterfactual approach to causality, is based on distance metrics for program executions. Experimental results
show that the power of the model checking engine can be used to provide assistance in understanding errors and to isolate
faulty portions of the source code. |
| |
Keywords: | Model checking Error explanation Fault localization Automated debugging |
本文献已被 SpringerLink 等数据库收录! |
|