{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T08:57:24Z","timestamp":1729673844376,"version":"3.28.0"},"reference-count":22,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1109\/tase.2017.8285629","type":"proceedings-article","created":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T17:54:03Z","timestamp":1518458043000},"page":"1-8","source":"Crossref","is-referenced-by-count":1,"title":["Assembly program verification for multiprocessors with relaxed memory model using SMT solver"],"prefix":"10.1109","author":[{"given":"Pattaravut","family":"Maleehuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuki","family":"Chiba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1007\/978-3-642-03359-9_27"},{"doi-asserted-by":"publisher","key":"ref11","DOI":"10.1145\/2658982.2527287"},{"key":"ref12","first-page":"146","author":"armando","year":"2006","journal-title":"Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1145\/2983990.2984025"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1145\/1250734.1250737"},{"key":"ref15","first-page":"1","article-title":"Stateless model checking for TSO and PSO","author":"abdulla","year":"2016","journal-title":"Acta Informatica"},{"key":"ref16","first-page":"134","author":"abdulla","year":"2016","journal-title":"Stateless Model Checking for POWER"},{"doi-asserted-by":"publisher","key":"ref17","DOI":"10.1145\/2814270.2814297"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1007\/978-3-642-39799-8_9"},{"doi-asserted-by":"publisher","key":"ref19","DOI":"10.1145\/1806596.1806635"},{"year":"1994","author":"may","journal-title":"The PowerPC Architecture A Specification for a New Family of RISC Processors","key":"ref4"},{"year":"2008","author":"limited","journal-title":"ARM Architecture Reference Manual ARMv7-A and ARMv7-R Edition","key":"ref3"},{"key":"ref6","first-page":"295","article-title":"SPARC International Inc","year":"1992","journal-title":"The SPARC architecture manual v8"},{"year":"1995","author":"gharachorloo","journal-title":"Designing Memory Consistency Models for Shared Memory Multiprocessors","key":"ref5"},{"year":"1992","author":"sites","journal-title":"Alpha Architecture Reference Manual","key":"ref8"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1109\/TC.1979.1675439"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1007\/978-3-642-03359-9_27"},{"year":"2012","author":"inria","journal-title":"A tutorial introduction to the arm and power relaxed memory models","key":"ref1"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/325096.325100","article-title":"Weak ordering - a new definition","volume":"18","author":"adve","year":"1990","journal-title":"ISCA '90 Proceedings of the 17th annual international symposium on Computer Architecture"},{"doi-asserted-by":"publisher","key":"ref20","DOI":"10.1016\/j.tcs.2008.03.013"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.1007\/s10703-011-0135-z"},{"doi-asserted-by":"publisher","key":"ref21","DOI":"10.1145\/2737924.2737975"}],"event":{"name":"2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)","start":{"date-parts":[[2017,9,13]]},"location":"Sophia Antipolis","end":{"date-parts":[[2017,9,15]]}},"container-title":["2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8277122\/8285614\/08285629.pdf?arnumber=8285629","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T17:21:58Z","timestamp":1570728118000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8285629\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/tase.2017.8285629","relation":{},"subject":[],"published":{"date-parts":[[2017,9]]}}}