This page intentionally left blank. Generating Abstract Explanations of Spurious Counterexamples in C Programs

Abstract. Counterexample driven renement is a promising technique to generate automatic abstractions for model checking software. A central problem in automating this approach is the re nement of models from spurious error traces. We present a solution to this problem for C pro-grams. 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.