Understanding counterexamples with explain

Alex Groce, Daniel Kroening, Flavio Lerda

Research output: Chapter in Book/Report/Conference proceedingChapter

45 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 languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRajeev Alur, Doron A. Peled
PublisherSpringer-Verlag
Pages453-456
Number of pages4
ISBN (Print)3540223428, 9783540223429
DOIs
StatePublished - 2004
Externally publishedYes

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Understanding counterexamples with explain'. Together they form a unique fingerprint.

Cite this