BMC with Memory Models as Modules

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

Researchers

Research units

  • fortiss GmbH
  • TU Braunschweig

Abstract

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.

Details

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
EventConference on Formal Methods in Computer-Aided Design - Austin, United States
Duration: 30 Oct 20182 Nov 2018
Conference number: 18

Conference

ConferenceConference on Formal Methods in Computer-Aided Design
Abbreviated titleFMCAD
CountryUnited States
CityAustin
Period30/10/201802/11/2018

    Research areas

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

ID: 32267588