Abstract: This work discusses analyzing counterexamples produced by model checking programs. An error trace alone is often insufficient to allow a programmer to easily diagnose and understand a bug in a program. This work introduces a search technique to find suitable "near" traces that either exhibit different versions of the error or reach the same control state without error. At present, the algorithim is explicit-state and concerned with safety properties only.

Once the sets of negative and positive traces are generated, various analysis methods are used to describe common elements of the traces to explain the bug. In particular, invariants, program points covered, and means of transforming positive traces into negative traces are computed. Errors in which thread-scheduling only is important can be identified, for instance.