BMC with Memory Models as Modules

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


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

Research units

  • fortiss GmbH
  • TU Braunschweig


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
Publication statusPublished - 4 Jan 2019
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

    Research areas

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

ID: 32267588