Counterexample guided abstraction refinement via program execution

Daniel Kroening, Alex Groce, Edmund Clarke

Research output: Chapter in Book/Report/Conference proceedingChapter

39 Scopus citations

Abstract

Software model checking tools based on a Counterexample Guided Abstraction Refinement (CEGAR) framework have attained considerable success in limited domains. However, scaling these approaches to larger programs with more complex data structures and initialization behavior has proven difficult. Explicit-state model checkers making use of states and operational semantics closely related to actual program execution have dealt with complex data types and semantic issues successfully, but do not deal as well with very large state spaces. This paper presents an approach to software model checking that actually executes the program in order to drive abstraction-refinement. The inputs required for the execution are derived from the abstract model. Driving the abstraction-refinement loop with a combination of constant-sized (and thus scalable) Boolean satisfiability-based simulation and actual program execution extends abstraction-based software model checking to a much wider array of programs than current tools can handle, in the case of programs containing errors. Experimental results from applying the CRunner tool, which implements execution-based refinement, to faulty and correct C programs demonstrate the practical utility of the idea.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsJim Davies, Wolfram Schulte, Mike Barnett
PublisherSpringer-Verlag
Pages224-238
Number of pages15
ISBN (Electronic)3540238417, 9783540238416
DOIs
StatePublished - 2004
Externally publishedYes

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Counterexample guided abstraction refinement via program execution'. Together they form a unique fingerprint.

Cite this