Alex David Groce

Error Explanation and Fault Localization with Distance Metrics Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund Clarke
Graduated: May 2005

Abstract:

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.

Thesis Committee:
Edmund Clarke (Chair)
Reid Simmons
David Garlan
Willem Visser (NASA Ames Research Center)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Formal methods, model checking, fault localization, automated debugging, distance metrics, bounded model checking