BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Standard

BMC for Weak Memory Models : Relation Analysis for Compact SMT Encodings. / Gavrilenko, Natalia; Ponce-de-León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland.

Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. toim. / Isil Dillig; Serdar Tasiran. Springer Verlag, 2019. s. 355-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11561 LNCS).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Harvard

Gavrilenko, N, Ponce-de-León, H, Furbach, F, Heljanko, K & Meyer, R 2019, BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. julkaisussa I Dillig & S Tasiran (toim), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vuosikerta. 11561 LNCS, Springer Verlag, Sivut 355-365, New York City, Yhdysvallat, 15/07/2019. https://doi.org/10.1007/978-3-030-25540-4_19

APA

Gavrilenko, N., Ponce-de-León, H., Furbach, F., Heljanko, K., & Meyer, R. (2019). BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. teoksessa I. Dillig, & S. Tasiran (Toimittajat), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings (Sivut 355-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11561 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-25540-4_19

Vancouver

Gavrilenko N, Ponce-de-León H, Furbach F, Heljanko K, Meyer R. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. julkaisussa Dillig I, Tasiran S, toimittajat, Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Springer Verlag. 2019. s. 355-365. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-25540-4_19

Author

Gavrilenko, Natalia ; Ponce-de-León, Hernán ; Furbach, Florian ; Heljanko, Keijo ; Meyer, Roland. / BMC for Weak Memory Models : Relation Analysis for Compact SMT Encodings. Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Toimittaja / Isil Dillig ; Serdar Tasiran. Springer Verlag, 2019. Sivut 355-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Bibtex - Lataa

@inproceedings{4e699328c9964f43a915b86b5091c913,
title = "BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings",
abstract = "We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.",
keywords = "BMC, CAT, Concurrency, SMT, Weak memory models",
author = "Natalia Gavrilenko and Hern{\'a}n Ponce-de-Le{\'o}n and Florian Furbach and Keijo Heljanko and Roland Meyer",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-25540-4_19",
language = "English",
isbn = "9783030255398",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "355--365",
editor = "Isil Dillig and Serdar Tasiran",
booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",

}

RIS - Lataa

TY - GEN

T1 - BMC for Weak Memory Models

T2 - Relation Analysis for Compact SMT Encodings

AU - Gavrilenko, Natalia

AU - Ponce-de-León, Hernán

AU - Furbach, Florian

AU - Heljanko, Keijo

AU - Meyer, Roland

PY - 2019/1/1

Y1 - 2019/1/1

N2 - We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.

AB - We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.

KW - BMC

KW - CAT

KW - Concurrency

KW - SMT

KW - Weak memory models

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

U2 - 10.1007/978-3-030-25540-4_19

DO - 10.1007/978-3-030-25540-4_19

M3 - Conference contribution

SN - 9783030255398

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 355

EP - 365

BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings

A2 - Dillig, Isil

A2 - Tasiran, Serdar

PB - Springer Verlag

ER -

ID: 36034523