BMC with Memory Models as Modules

Näytä kaikki kuvailutiedot



Pysyväisosoite

http://hdl.handle.net/10138/310453

Lähdeviite

Ponce-de-Leon , H , Furbach , F , Heljanko , K & Meyer , R 2018 , BMC with Memory Models as Modules . in N Bjørner & A Gurfinkel (eds) , Proceedings of the 18th Conference onFormal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 – November 2, 2018 . IEEE , pp. 22-30 , Conference on Formal Methods in Computer-Aided Design , Austin , Texas , United States , 30/10/2018 . https://doi.org/10.23919/FMCAD.2018.8603021

Julkaisun nimi: BMC with Memory Models as Modules
Tekijä: Ponce-de-Leon, Hernan; Furbach, Florian; Heljanko, Keijo; Meyer, Roland
Muu tekijä: Bjørner , Nikolaj
Gurfinkel, Arie
Tekijän organisaatio: Helsinki Institute for Information Technology
Department of Computer Science
Julkaisija: IEEE
Päiväys: 2018
Kieli: eng
Sivumäärä: 9
Kuuluu julkaisusarjaan: Proceedings of the 18th Conference onFormal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 – November 2, 2018
ISBN: 978-1-5386-7567-0
978-0-9835678-8-2
DOI-tunniste: https://doi.org/10.23919/FMCAD.2018.8603021
URI: http://hdl.handle.net/10138/310453
Tiivistelmä: 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.
Avainsanat: Memory models
CAT
concurrent programs
bounded model checking
SMT encodings
CHECKING
VERIFICATION
113 Computer and information sciences
Vertaisarvioitu: Kyllä
Tekijänoikeustiedot: cc_by
Pääsyrajoitteet: openAccess
Rinnakkaistallennettu versio: publishedVersion


Tiedostot

Latausmäärä yhteensä: Ladataan...

Tiedosto(t) Koko Formaatti Näytä
08603021.pdf 320.2KB PDF Avaa tiedosto

Viite kuuluu kokoelmiin:

Näytä kaikki kuvailutiedot