Understanding counterexamples with explain

Alex Groce; Daniel Kroening; Flavio Lerda

doi:10.1007/978-3-540-27813-9_35

Understanding counterexamples with explain

Alex Groce, Daniel Kroening, Flavio Lerda

Research output: Chapter in Book/Report/Conference proceeding › Chapter

48 Scopus citations

Abstract

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.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Rajeev Alur, Doron A. Peled
Publisher	Springer-Verlag
Pages	453-456
Number of pages	4
ISBN (Print)	3540223428, 9783540223429
DOIs	https://doi.org/10.1007/978-3-540-27813-9_35
State	Published - 2004
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3114
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-27813-9_35

Cite this

Groce, A., Kroening, D., & Lerda, F. (2004). Understanding counterexamples with explain. In R. Alur, & D. A. Peled (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 453-456). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3114). Springer-Verlag. https://doi.org/10.1007/978-3-540-27813-9_35

Understanding counterexamples with explain. / Groce, Alex; Kroening, Daniel; Lerda, Flavio.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Rajeev Alur; Doron A. Peled. Springer-Verlag, 2004. p. 453-456 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3114).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Groce, A, Kroening, D & Lerda, F 2004, Understanding counterexamples with explain. in R Alur & DA Peled (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3114, Springer-Verlag, pp. 453-456. https://doi.org/10.1007/978-3-540-27813-9_35

Groce A, Kroening D, Lerda F. Understanding counterexamples with explain. In Alur R, Peled DA, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag. 2004. p. 453-456. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-27813-9_35

Groce, Alex ; Kroening, Daniel ; Lerda, Flavio. / Understanding counterexamples with explain. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Rajeev Alur ; Doron A. Peled. Springer-Verlag, 2004. pp. 453-456 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{c9686d373702418f8b7946a43b1de1e6,

title = "Understanding counterexamples with explain",

abstract = "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.",

author = "Alex Groce and Daniel Kroening and Flavio Lerda",

year = "2004",

doi = "10.1007/978-3-540-27813-9_35",

language = "English (US)",

isbn = "3540223428",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "453--456",

editor = "Rajeev Alur and Peled, {Doron A.}",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Understanding counterexamples with explain

AU - Groce, Alex

AU - Kroening, Daniel

AU - Lerda, Flavio

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35048853191&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35048853191&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-27813-9_35

DO - 10.1007/978-3-540-27813-9_35

M3 - Chapter

AN - SCOPUS:35048853191

SN - 3540223428

SN - 9783540223429

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 453

EP - 456

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Alur, Rajeev

A2 - Peled, Doron A.

PB - Springer-Verlag

ER -

Understanding counterexamples with explain

Abstract

Publication series

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this