Understanding Counterexamples with explain

The counterexamples produced by model checkers are often lengthy and difficult to understand. In practical verification, showing the existence of a (potential) bug is not enough: the error must be understood, determined to not be a result of faulty specification or assumptions, and, finally, located and corrected. The explain tool uses distance metrics on program executions to provide automated assistance in understanding and localizing errors in ANSI-C programs. explain is integrated with CBMC, a bounded model checker for the C language, and features a GUI front-end that presents error explanations to the user.