A New Refinement Strategy for CEGAR-Based Industrial Model Checking

Martin Leucker; Grigory Markin; Martin R. Neuhäußer

doi:10.1007/978-3-319-26287-1_10

A New Refinement Strategy for CEGAR-Based Industrial Model Checking

Martin Leucker, Grigory Markin, Martin R. Neuhäußer

Institute of Software Engineering and Programming Languages

Siemens Healthcare

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.

Original language	English
Title of host publication	Hardware and Software: Verification and Testing
Editors	N. Piterman
Number of pages	16
Volume	9434
Place of Publication	Cham
Publisher	Springer Verlag
Publication date	28.11.2015
Pages	155-170
ISBN (Print)	978-3-319-26286-4
ISBN (Electronic)	978-3-319-26287-1
DOIs	https://doi.org/10.1007/978-3-319-26287-1_10
Publication status	Published - 28.11.2015
Event	11th International Haifa Verification Conference - Haifa, Israel Duration: 17.11.2015 → 19.11.2015 Conference number: 154279

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-319-26287-1_10

Cite this

@inproceedings{7782e111b0644899afa27391573e2449,

title = "A New Refinement Strategy for CEGAR-Based Industrial Model Checking",

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{\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.",

author = "Martin Leucker and Grigory Markin and Neuh{\"a}u{\ss}er, {Martin R.}",

year = "2015",

month = nov,

day = "28",

doi = "10.1007/978-3-319-26287-1_10",

language = "English",

isbn = "978-3-319-26286-4",

volume = "9434",

series = "Lecture Notes in Computer Science ",

publisher = "Springer Verlag",

pages = "155--170",

editor = "{Piterman }, { N.}",

booktitle = "Hardware and Software: Verification and Testing",

note = "11th International Haifa Verification Conference , HVC 2015 ; Conference date: 17-11-2015 Through 19-11-2015",

}

Leucker, M, Markin, G & Neuhäußer, MR 2015, A New Refinement Strategy for CEGAR-Based Industrial Model Checking. in N Piterman (ed.), Hardware and Software: Verification and Testing. vol. 9434, Lecture Notes in Computer Science , vol. 9434, Springer Verlag, Cham, pp. 155-170, 11th International Haifa Verification Conference , Haifa, Israel, 17.11.15. https://doi.org/10.1007/978-3-319-26287-1_10

A New Refinement Strategy for CEGAR-Based Industrial Model Checking. / Leucker, Martin; Markin, Grigory; Neuhäußer, Martin R.
Hardware and Software: Verification and Testing. ed. / N. Piterman . Vol. 9434 Cham: Springer Verlag, 2015. p. 155-170 (Lecture Notes in Computer Science ; Vol. 9434).

Research output: Chapters in Books/Reports/Conference Proceedings › Conference contribution › peer-review

TY - GEN

T1 - A New Refinement Strategy for CEGAR-Based Industrial Model Checking

AU - Leucker, Martin

AU - Markin, Grigory

AU - Neuhäußer, Martin R.

N1 - Conference code: 154279

PY - 2015/11/28

Y1 - 2015/11/28

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

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

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-84950248257&origin=inward&txGid=042862074cda5569705290bdf87004b2

U2 - 10.1007/978-3-319-26287-1_10

DO - 10.1007/978-3-319-26287-1_10

M3 - Conference contribution

SN - 978-3-319-26286-4

VL - 9434

T3 - Lecture Notes in Computer Science

SP - 155

EP - 170

BT - Hardware and Software: Verification and Testing

A2 - Piterman , N.

PB - Springer Verlag

CY - Cham

T2 - 11th International Haifa Verification Conference

Y2 - 17 November 2015 through 19 November 2015

ER -

A New Refinement Strategy for CEGAR-Based Industrial Model Checking

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this