BMC with Memory Models as Modules

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

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


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 languageEnglish
Title of host publicationProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
EditorsNikolaj Bjorner, Arie Gurfinkel
Number of pages9
ISBN (Electronic)9780983567882
Publication statusPublished - 2018
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Formal Methods in Computer-Aided Design - Austin, United States
Duration: 30 Oct 20182 Nov 2018
Conference number: 18


ConferenceInternational Conference on Formal Methods in Computer-Aided Design
Abbreviated titleFMCAD
CountryUnited States


  • Bounded model checking
  • CAT
  • Concurrent programs
  • Memory models
  • SMT encodings

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

Cite this