Learning Centre

BMC for Weak Memory Models

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Gavrilenko, Natalia
dc.contributor.author Ponce-de-León, Hernán
dc.contributor.author Furbach, Florian
dc.contributor.author Heljanko, Keijo
dc.contributor.author Meyer, Roland
dc.contributor.editor Dillig, Isil
dc.contributor.editor Tasiran, Serdar
dc.date.accessioned 2019-08-15T08:22:58Z
dc.date.available 2019-08-15T08:22:58Z
dc.date.issued 2019-01-01
dc.identifier.citation 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 . in I Dillig & S Tasiran (eds) , 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) , vol. 11561 LNCS , SPRINGER , pp. 355-365 , International Conference on Computer Aided Verification , New York City , New York , United States , 15/07/2019 . https://doi.org/10.1007/978-3-030-25540-4_19 en
dc.identifier.isbn 9783030255398
dc.identifier.issn 0302-9743
dc.identifier.issn 1611-3349
dc.identifier.other PURE UUID: 4e699328-c996-4f43-a915-b86b5091c913
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/4e699328-c996-4f43-a915-b86b5091c913
dc.identifier.other PURE LINK: http://www.scopus.com/inward/record.url?scp=85069884055&partnerID=8YFLogxK
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/36034525/Gavrilenko2019_Chapter_BMCForWeakMemoryModelsRelation.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/39668
dc.description.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. en
dc.format.extent 11
dc.format.extent 355-365
dc.format.mimetype application/pdf
dc.language.iso en en
dc.relation.ispartof International Conference on Computer Aided Verification en
dc.relation.ispartofseries Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings en
dc.relation.ispartofseries Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) en
dc.relation.ispartofseries Volume 11561 LNCS en
dc.rights openAccess en
dc.title BMC for Weak Memory Models en
dc.type A4 Artikkeli konferenssijulkaisussa fi
dc.description.version Peer reviewed en
dc.contributor.department Department of Computer Science
dc.contributor.department fortiss GmbH
dc.contributor.department TU Braunschweig
dc.contributor.department University of Helsinki
dc.subject.keyword BMC
dc.subject.keyword CAT
dc.subject.keyword Concurrency
dc.subject.keyword SMT
dc.subject.keyword Weak memory models
dc.identifier.urn URN:NBN:fi:aalto-201908154713
dc.identifier.doi 10.1007/978-3-030-25540-4_19
dc.type.version publishedVersion

Files in this item

Files Size Format View

There are no open access files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication