BMC with Memory Models as Modules

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Tutkijat

Organisaatiot

  • fortiss GmbH
  • TU Braunschweig

Kuvaus

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.

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
ToimittajatNikolaj Bjorner, Arie Gurfinkel
TilaJulkaistu - 4 tammikuuta 2019
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Formal Methods in Computer-Aided Design - Austin, Yhdysvallat
Kesto: 30 lokakuuta 20182 marraskuuta 2018
Konferenssinumero: 18

Conference

ConferenceInternational Conference on Formal Methods in Computer-Aided Design
LyhennettäFMCAD
MaaYhdysvallat
KaupunkiAustin
Ajanjakso30/10/201802/11/2018

ID: 32267588