What Went Wrong: Explaining Counterexamples

Abstract

Model checking, initially successful in the field of hardware design, has recently been applied to software. One of the chief advantages of model checking is the production of counterexamples demonstrating that a system does not satisfy a speci cation. 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 nding 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 identi cation of portions of the source code crucial to distinguishing failing and succeeding runs, di erences in invariants between failing and non-failing runs, and information on the necessary changes in scheduling and environmental actions needed to cause suc- cessful runs to fail. In addition, this analysis allows a classi cation of errors by features such as whether they are purely concurrent (i.e. can be induced by changing only thread scheduling).