BMC with Memory Models as Modules

Show simple item record Ponce-de-Leon, Hernan Furbach, Florian Heljanko, Keijo Meyer, Roland
dc.contributor.editor Bjørner , Nikolaj
dc.contributor.editor Gurfinkel, Arie 2020-01-27T14:30:02Z 2020-01-27T14:30:02Z 2018
dc.identifier.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 .
dc.identifier.citation conference
dc.identifier.other PURE: 130810137
dc.identifier.other PURE UUID: ac674dc1-c2a8-45e3-9ae0-ca115a8b251d
dc.identifier.other WOS: 000493916300009
dc.identifier.other ORCID: /0000-0002-4547-2701/work/68617336
dc.identifier.other Scopus: 85061650175
dc.description.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. en
dc.format.extent 9
dc.language.iso eng
dc.publisher IEEE
dc.relation.ispartof Proceedings of the 18th Conference onFormal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 – November 2, 2018
dc.relation.isversionof 978-1-5386-7567-0
dc.relation.isversionof 978-0-9835678-8-2
dc.rights cc_by
dc.rights.uri info:eu-repo/semantics/openAccess
dc.subject Memory models
dc.subject CAT
dc.subject concurrent programs
dc.subject bounded model checking
dc.subject SMT encodings
dc.subject CHECKING
dc.subject 113 Computer and information sciences
dc.title BMC with Memory Models as Modules en
dc.type Conference contribution
dc.contributor.organization Helsinki Institute for Information Technology
dc.contributor.organization Department of Computer Science
dc.description.reviewstatus Peer reviewed
dc.rights.accesslevel openAccess
dc.type.version publishedVersion

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 simple item record