BMC with Memory Models as Modules

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

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

Abstrakti

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.

AlkuperäiskieliEnglanti
OtsikkoProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
ToimittajatNikolaj Bjorner, Arie Gurfinkel
KustantajaIEEE
Sivut22-30
Sivumäärä9
ISBN (elektroninen)9780983567882
DOI - pysyväislinkit
TilaJulkaistu - 2018
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

Sormenjälki Sukella tutkimusaiheisiin 'BMC with Memory Models as Modules'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä