Download: PDF.
“What Went Wrong: Explaining Counterexamples”
by
Alex Groce
and
Willem Visser.
In SPIN 2003: 10th International SPIN Workshop on Model Checking of
Software, (Portland, Oregon), May 2003, pp. 121-135.
A previous version appeared as
“What went wrong: Explaining counterexamples”
by
Alex Groce
and
Willem Visser,
RIACS.
USRA technical report 02-08, 2002.
One of the chief advantages of model checking is the production of counterexamples demonstrating that a system does not satisfy a specification. However, it may require a great deal of human effort to extract the essence of an error from even a detailed source-level trace of a failing run. We use an automated method for finding multiple versions of an error (and similar executions that do not produce an error), and analyze these executions to produce a more succinct description of the key elements of the error. The description produced includes identification of portions of the source code crucial to distinguishing failing and succeeding runs, differences in invariants between failing and non-failing runs, and information on the necessary changes in scheduling and environmental actions needed to cause successful runs to fail.
Download: PDF.
BibTeX entry:
@inproceedings{GroceV2003,
author = {Alex Groce and Willem Visser},
title = {What Went Wrong: Explaining Counterexamples},
booktitle = {SPIN 2003: 10th International SPIN Workshop on Model
Checking of Software},
pages = {121--135},
address = {Portland, Oregon},
month = may,
year = {2003}
}