BMC with Memory Models as Modules

Visa fullständig post



Permalänk

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

Citation

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

Titel: BMC with Memory Models as Modules
Författare: Ponce-de-Leon, Hernan; Furbach, Florian; Heljanko, Keijo; Meyer, Roland
Medarbetare: Bjørner , Nikolaj
Gurfinkel, Arie
Upphovmannens organisation: Helsinki Institute for Information Technology
Department of Computer Science
Utgivare: IEEE
Datum: 2018
Språk: eng
Sidantal: 9
Tillhör serie: 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: https://doi.org/10.23919/FMCAD.2018.8603021
Permanenta länken (URI): http://hdl.handle.net/10138/310453
Abstrakt: 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.
Subject: Memory models
CAT
concurrent programs
bounded model checking
SMT encodings
CHECKING
VERIFICATION
113 Computer and information sciences
Referentgranskad: Ja
Licens: cc_by
Användningsbegränsning: openAccess
Parallelpublicerad version: publishedVersion


Filer under denna titel

Totalt antal nerladdningar: Laddar...

Filer Storlek Format Granska
08603021.pdf 320.2Kb PDF Granska/Öppna

Detta dokument registreras i samling:

Visa fullständig post