A New Refinement Strategy for CEGAR-Based Industrial Model Checking

TitleA New Refinement Strategy for CEGAR-Based Industrial Model Checking
Publication TypeBook Chapter
Year of Publication2015
AuthorsMartin, L, Grigory, M, R., NMartin
Book TitleHardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings
Pagination155–170
PublisherSpringer International Publishing
CityCham
ISBN Number978-3-319-26287-1
Abstract

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’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.

URLhttp://dx.doi.org/10.1007/978-3-319-26287-1_10
DOI10.1007/978-3-319-26287-1_10
Bibtex: 
@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.}
}