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.

PDF file

PostScript file

Details