BMC with Memory Models as Modules

Show full item record



Permalink

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 , United States , 30/10/2018 . https://doi.org/10.23919/FMCAD.2018.8603021

Title: BMC with Memory Models as Modules
Author: Ponce-de-Leon, Hernan; Furbach, Florian; Heljanko, Keijo; Meyer, Roland
Editor: Bjørner, Nikolaj; Gurfinkel, Arie
Contributor: University of Helsinki, Helsinki Institute for Information Technology
Publisher: IEEE
Date: 2018
Language: eng
Number of pages: 9
Belongs to series: 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
URI: http://hdl.handle.net/10138/310453
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.
Subject: Memory models
CAT
concurrent programs
bounded model checking
SMT encodings
CHECKING
VERIFICATION
113 Computer and information sciences
Rights:


Files in this item

Total number of downloads: Loading...

Files Size Format View
08603021.pdf 320.2Kb PDF View/Open

This item appears in the following Collection(s)

Show full item record