Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

CAV
2004
Springer

favoriteEmaildiscussreport

77views Hardware» more CAV 2004»

Understanding Counterexamples with explain

13 years 9 months ago

Understanding Counterexamples with explain

Download www.cs.cmu.edu

The counterexamples produced by model checkers are often lengthy and diﬃcult to understand. In practical veriﬁcation, showing the existence of a (potential) bug is not enough: the error must be understood, determined to not be a result of faulty speciﬁcation or assumptions, and, ﬁnally, 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

Real-time Traffic

CAV 2004 | Faulty Speciﬁcation | Formal Methods | Model Checker | Tool Uses Distance |

claim paper

Related Content

» Computation of minimal counterexamples by using black box techniques and symbolic methods

» Explaining Counterexamples Using Causality

» Explaining abstract counterexamples

» Counterexample Explanation by Anomaly Detection

» Trustworthy online controlled experiments five puzzling outcomes explained

» Shortest Counterexamples for Symbolic Model Checking of LTL with Past

» On Validity of Program Transformations in the Java Memory Model

» Witness and Counterexample Automata for ACTL

» Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models

Post Info
More Details (n/a)

Added	01 Jul 2010
Updated	01 Jul 2010
Type	Conference
Year	2004
Where	CAV
Authors	Alex Groce, Daniel Kroening, Flavio Lerda

Comments (0)