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

Natalia Gavrilenko*, Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

16 Citations (Scopus)
105 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
Number of pages11
ISBN (Print)9783030255398
Publication statusPublished - 1 Jan 2019
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Computer Aided Verification - New York City, United States
Duration: 15 Jul 201918 Jul 2019
Conference number: 31

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11561 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Computer Aided Verification
Abbreviated titleCAV
Country/TerritoryUnited States
CityNew York City


  • BMC
  • CAT
  • Concurrency
  • SMT
  • Weak memory models


Dive into the research topics of 'BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings'. Together they form a unique fingerprint.

Cite this