Counterexample-Guided Abstraction Refinement Export

@incollection{clarke2000counterexample, abstract = {We present an automatic iterative abstraction-refinement methodology in which the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or ” spurious”) counterexamples. We devise new symbolic techniques which analyze such counterexamples and refine the abstract model correspondingly. The refinement algorithm keeps the size of the abstract state space small due to the use of abstraction functions which distinguish many degrees of abstraction for each program variable. We describe an implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.}, author = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and Veith, Helmut}, citeulike-article-id = {5790265}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/10722167_15}, citeulike-linkout-1 = {http://www.springerlink.com/content/d833527r467g7261}, doi = {10.1007/10722167_15}, journal = {Computer Aided Verification}, keywords = {abstraction-refinement, model-checking, verification}, pages = {154--169}, posted-at = {2009-11-06 17:29:28}, priority = {2}, title = {Counterexample-Guided Abstraction Refinement}, url = {http://dx.doi.org/10.1007/10722167_15}, year = {2000} }

TY - CHAP ID - clarke2000counterexample L3 - citeulike-article-id:5790265 N2 - We present an automatic iterative abstraction-refinement methodology in which the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or “spurious”) counterexamples. We devise new symbolic techniques which analyze such counterexamples and refine the abstract model correspondingly. The refinement algorithm keeps the size of the abstract state space small due to the use of abstraction functions which distinguish many degrees of abstraction for each program variable. We describe an implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach. JF - Computer Aided Verification EP - 169 TI - Counterexample-Guided Abstraction Refinement SP - 154 KW - abstraction-refinement KW - model-checking KW - verification AU - Clarke, Edmund AU - Grumberg, Orna AU - Jha, Somesh AU - Lu, Yuan AU - Veith, Helmut PY - 2000/// UR - http://dx.doi.org/10.1007/10722167_15 ER -