Generating Abstract Explanations of Spurious Counterexamples in C Programs Export

@article{citeulike:2895493, abstract = {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.}, author = {Ball, Thomas and Rajamani, Sriram K.}, citeulike-article-id = {2895493}, citeulike-linkout-0 = {http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSR-TR-2002-09}, keywords = {2002, abstraction, booleanprogram, slam}, posted-at = {2008-06-15 07:43:56}, priority = {2}, title = {Generating Abstract Explanations of Spurious Counterexamples in C Programs}, url = {http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSR-TR-2002-09}, year = {2002} }

TY - JOUR ID - citeulike:2895493 L3 - citeulike-article-id:2895493 N2 - 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. TI - Generating Abstract Explanations of Spurious Counterexamples in C Programs KW - 2002 KW - abstraction KW - booleanprogram KW - slam AU - Ball, Thomas AU - Rajamani, Sriram PY - 2002/// UR - http://research.microsoft.com/research/pubs/view.aspx?msr_tr_id=MSR-TR-2002-09 ER -