When a program's correctness cannot be verified, a model checker produces a counterexample that shows a specific instance of undesirable behavior. Given this counterexample, it is up to the user to understand and correct the problem. This can be a very difficult task. The error may be in the specification, the environment or modeling assumptions, or the program itself. If the error is determined to be real, the fault localization problem remains: before the problem can be corrected, the faulty portion of the code must be identified. Industrial experience and research show that debugging is a time-consuming and difficult step of development even for expert programmers. The counterexample provided by a model checker does not provide sufficient information to ease this task. Counterexample traces can be very long and difficult to read, and often include hundreds or potentially even thousands of lines of code unrelated to the error.

Error explanation is the effort to provide automated assistance in moving from a counterexample to a correction for an error. Explanation provides information as to the cause of an error and includes fault localization by indicating likely problem areas in the source code or specification.

This work presents a novel and successful approach to error explanation. The approach is based on distance metrics for program executions. The use of distance metrics is inspired by the counterfactual theory of causality proposed by philosopher David Lewis, and the insights gained from previous work on providing practical error explanation.

282 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu