Understanding Counterexamples with explain

11 years 5 months ago
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.
Alex Groce, Daniel Kroening, Flavio Lerda
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Alex Groce, Daniel Kroening, Flavio Lerda
Comments (0)