BMC with Memory Models as Modules

Hernan Ponce-De-Leon; Florian Furbach; Keijo Heljanko; Roland Meyer

doi:10.23919/FMCAD.2018.8603021

BMC with Memory Models as Modules

Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko, Roland Meyer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review

Abstract

This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.

Original language	English
Title of host publication	Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
Editors	Nikolaj Bjorner, Arie Gurfinkel
Publisher	IEEE
Pages	22-30
Number of pages	9
ISBN (Electronic)	9780983567882
DOIs	https://doi.org/10.23919/FMCAD.2018.8603021
Publication status	Published - 2018
MoE publication type	A4 Article in a conference publication
Event	International Conference on Formal Methods in Computer-Aided Design - Austin, United States Duration: 30 Oct 2018 → 2 Nov 2018 Conference number: 18

Conference

Conference	International Conference on Formal Methods in Computer-Aided Design
Abbreviated title	FMCAD
Country	United States
City	Austin
Period	30/10/2018 → 02/11/2018

Keywords

Bounded model checking
CAT
Concurrent programs
Memory models
SMT encodings

Access to Document

10.23919/FMCAD.2018.8603021

Fingerprint Dive into the research topics of 'BMC with Memory Models as Modules'. Together they form a unique fingerprint.

Cite this

@inproceedings{d0695c5bb6784a278789eaedd5f7199b,

title = "BMC with Memory Models as Modules",

abstract = "This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.",

keywords = "Bounded model checking, CAT, Concurrent programs, Memory models, SMT encodings",

author = "Hernan Ponce-De-Leon and Florian Furbach and Keijo Heljanko and Roland Meyer",

year = "2018",

doi = "10.23919/FMCAD.2018.8603021",

language = "English",

pages = "22--30",

editor = "Nikolaj Bjorner and Arie Gurfinkel",

booktitle = "Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018",

publisher = "IEEE",

address = "United States",

note = "International Conference on Formal Methods in Computer-Aided Design, FMCAD ; Conference date: 30-10-2018 Through 02-11-2018",

}

Ponce-De-Leon, H, Furbach, F, Heljanko, K & Meyer, R 2018, BMC with Memory Models as Modules. in N Bjorner & A Gurfinkel (eds), Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018., 8603021, IEEE, pp. 22-30, International Conference on Formal Methods in Computer-Aided Design, Austin, United States, 30/10/2018. https://doi.org/10.23919/FMCAD.2018.8603021

BMC with Memory Models as Modules. / Ponce-De-Leon, Hernan; Furbach, Florian; Heljanko, Keijo; Meyer, Roland.

Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018. ed. / Nikolaj Bjorner; Arie Gurfinkel. IEEE, 2018. p. 22-30 8603021.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review

TY - GEN

T1 - BMC with Memory Models as Modules

AU - Ponce-De-Leon, Hernan

AU - Furbach, Florian

AU - Heljanko, Keijo

AU - Meyer, Roland

N1 - Conference code: 18

PY - 2018

Y1 - 2018

N2 - This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.

AB - This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.

KW - Bounded model checking

KW - CAT

KW - Concurrent programs

KW - Memory models

KW - SMT encodings

UR - http://www.scopus.com/inward/record.url?scp=85061650175&partnerID=8YFLogxK

U2 - 10.23919/FMCAD.2018.8603021

DO - 10.23919/FMCAD.2018.8603021

M3 - Conference contribution

AN - SCOPUS:85061650175

SP - 22

EP - 30

BT - Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

A2 - Bjorner, Nikolaj

A2 - Gurfinkel, Arie

PB - IEEE

T2 - International Conference on Formal Methods in Computer-Aided Design

Y2 - 30 October 2018 through 2 November 2018

ER -