{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:07Z","timestamp":1784830747399,"version":"3.55.0"},"reference-count":50,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603021","type":"proceedings-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T01:33:52Z","timestamp":1546997632000},"page":"1-9","source":"Crossref","is-referenced-by-count":15,"title":["BMC with Memory Models as Modules"],"prefix":"10.23919","author":[{"given":"Hernan","family":"Ponce-de-Leon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Furbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","article-title":"Portability analysis for axiomatic memory models. PORTHOS: One tool for all models","author":"de le\u00f3n","year":"2017","journal-title":"CoRR"},{"key":"ref38","first-page":"1","article-title":"Partially redundant fence elimination for x86, ARM, and Power processors","author":"morisset","year":"2017","journal-title":"CC"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2261417.2261438"},{"key":"ref32","first-page":"17:1","article-title":"Effective stateless model checking for C\/C++ concurrency","volume":"2","author":"kokologiannakis","year":"2018","journal-title":"PACMPL"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"ref30","first-page":"20","article-title":"Satcheck: Sat-directed stateless model checking for sc and tso","author":"demsky","year":"2015","journal-title":"OOPSLA"},{"key":"ref37","article-title":"Counterexamples and proof loophole for the C\/C++ to POWER and armv7 trailing-sync compiler mappings","author":"manerkar","year":"2016","journal-title":"CoRR"},{"key":"ref36","first-page":"495","article-title":"An axiomatic memory model for POWER multiprocessors","author":"mador-haim","year":"2012","journal-title":"CAV volume 7358 of LNCS"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"ref34","first-page":"618","article-title":"Repairing sequential consistency in C\/C++11","author":"lahav","year":"2017","journal-title":"PLDI"},{"key":"ref28","first-page":"449","article-title":"Effective abstractions for verification under relaxed memory models","author":"dan","year":"2015","journal-title":"VMCAI volume 8931 of LNCS"},{"key":"ref27","first-page":"84","article-title":"Predicate abstraction for relaxed memory models","author":"dan","year":"2013","journal-title":"SAS volume 7935 of LNCS"},{"key":"ref29","first-page":"337","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"TACAS Volume 4963 of LNCS"},{"key":"ref2","first-page":"353","article-title":"Stateless model checking for TSO and PSO","author":"abdulla","year":"2015","journal-title":"TACAS volume 9035 of LNCS"},{"key":"ref1","year":"0","journal-title":"C\/C++ 11 mappings to processors"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003493"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"ref21","first-page":"533","article-title":"Checking and enforcing robustness against TSO","author":"bouajjani","year":"2013","journal-title":"ESOP Volume 7792 of LNCS"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref23","first-page":"107","article-title":"Effective program verification for relaxed memory models","author":"burckhardt","year":"2008","journal-title":"CAV volume 5123 of LNCS"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_19"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_12"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"ref10","first-page":"508","article-title":"Don’t sit on the fence - A static analysis approach to automatic fence insertion","author":"alglave","year":"2014","journal-title":"CAV'14 volume 8559 of LNCS"},{"key":"ref11","first-page":"141","article-title":"Partial orders for efficient bounded model checking of concurrent software","author":"alglave","year":"2013","journal-title":"CAV Volume 8044 of LNCS"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/978-3-319-66706-5_15","article-title":"Portability analysis for weak memory models. PORTHOS: One tool for all models","author":"de le\u00f3n","year":"2017","journal-title":"SAS volume 10422 of Lecture Notes in Computer Science"},{"key":"ref12","author":"alglave","year":"0","journal-title":"The diy7 tool suite"},{"key":"ref13","first-page":"50","article-title":"Stability in weak memory models","author":"alglave","year":"2011","journal-title":"CAV Volume 6806 of LNCS"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"ref17","first-page":"825","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability Volume 185 of Frontiers in Artificial Intelligence and Applications"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"ref4","first-page":"204","article-title":"Counter-example guided fence insertion under TSO","author":"abdulla","year":"2012","journal-title":"TACAS volume 7214 of LNCS"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_13"},{"key":"ref6","first-page":"134","article-title":"Stateless model checking for POWER","author":"abdulla","year":"2016","journal-title":"CAV volume 9780 of LNCS"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_37"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_1"},{"key":"ref7","author":"alglave","year":"2010","journal-title":"A Shared Memory Poetics"},{"key":"ref49","first-page":"190","article-title":"Automatically comparing memory consistency models","author":"wickerson","year":"2017","journal-title":"POPL"},{"key":"ref9","article-title":"Syntax and semantics of the weak consistency model specification language CAT","author":"alglave","year":"2016","journal-title":"CoRR"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660243"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"ref48","first-page":"867","article-title":"Relaxed separation logic: A program logic for C11 concurrency","author":"vafeiadis","year":"2013","journal-title":"OOPSLA"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"ref42","first-page":"379","article-title":"The semantics of x86-CC multiprocessor machine code","author":"sarkar","year":"2009","journal-title":"POPL"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139166386"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603021.pdf?arnumber=8603021","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T00:31:33Z","timestamp":1643157093000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603021\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":50,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603021","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}