A New Refinement Strategy for CEGAR-Based Industrial Model Checking

@inbook {1215,
	title = {A New Refinement Strategy for CEGAR-Based Industrial Model Checking},
	booktitle = {Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings},
	year = {2015},
	pages = {155{\textendash}170},
	publisher = {Springer International Publishing},
	organization = {Springer International Publishing},
	address = {Cham},
	abstract = {<p><span style="color: rgb(51, 51, 51); font-family: {\textquoteright}Helvetica Neue{\textquoteright}, Arial, Helvetica, sans-serif; font-size: 13px; background-color: rgb(255, 255, 255);">This paper presents a novel refinement strategy in the setting of counterexample-guided abstraction refinement (CEGAR)-based model checking. More specifically, the approach shown builds on lazy abstraction in the context of predicate abstraction. While the concept of interpolants is typically used for refinement, this paper employs unsatisfiability cores together with weakest preconditions. The new refinement technique is especially applicable in the setting where interpolants are hard to compute, such as for McCarthy{\textquoteright}s theory of arrays or for the theory of fixed-width bit vectors. It is implemented within a model-checking tool developed for the verification of industrial-critical systems and outperforms current refinement strategies on several examples.</span></p>
},
	isbn = {978-3-319-26287-1},
	doi = {10.1007/978-3-319-26287-1_10},
	url = {http://dx.doi.org/10.1007/978-3-319-26287-1_10},
	author = {Leucker Martin and Markin Grigory and Neuh{\"a}u{\ss}er Martin R.}
}