Generating Abstract Explanations of Spurious Counterexamples in C Programs

Counterexample driven refinement is a promising technique to generate automatic abstractions for model checking software. A central problem in automating this approach is the refinement of models from spurious error traces. We present a solution to this problem for C programs. Our solution introduces compile time names for run time values, and handles all constructs in the C programming language. We present Newton, an implementation of our solution, and empirical results from running Newton on several C programs.

tr-2002-09.pdf
PDF file
tr-2002-09.ps
PostScript file

Details

TypeTechReport
NumberMSR-TR-2002-09
Pages15
InstitutionMicrosoft Research
> Publications > Generating Abstract Explanations of Spurious Counterexamples in C Programs