{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T16:54:23Z","timestamp":1793033663289,"version":"4.5.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,17]],"date-time":"2010-01-17T00:00:00Z","timestamp":1263686400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,17]]},"DOI":"10.1145\/1706299.1706303","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T15:15:04Z","timestamp":1263914104000},"page":"7-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":80,"title":["On the verification problem for weak memory models"],"prefix":"10.1145","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[{"name":"LIAFA, University of Paris Diderot, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[{"name":"LIAFA, University of Paris Diderot, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Burckhardt","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Madanlal","family":"Musuvathi","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287591"},{"key":"e_1_3_2_1_2_1","first-page":"316","volume-title":"ICALP, LNCS 820","author":"Abdulla P.","year":"1994","unstructured":"P. Abdulla and B. Jonsson . Undecidable verification problems for programs with unreliable channels . In ICALP, LNCS 820 , pages 316 -- 327 . Springer , 1994 . P. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. In ICALP, LNCS 820, pages 316--327. Springer, 1994."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0053"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788796"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788833"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_11"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_1_10_1","volume-title":"International Symposium on Computer Architecture (ISCA)","author":"Otool S. Hangal","year":"2004","unstructured":"S. Hangal et al. TS Otool : A program for verifying memory systems using the memory consistency model . In International Symposium on Computer Architecture (ISCA) , 2004 . S. Hangal et al. TSOtool: A program for verifying memory systems using the memory consistency model. In International Symposium on Computer Architecture (ISCA), 2004."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_4"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"e_1_3_2_1_14_1","first-page":"317","volume-title":"Parallel and Distributed Processing","author":"Gibbons P.B.","year":"1992","unstructured":"P.B. Gibbons and E. Korach . The complexity of sequential consistency . In Parallel and Distributed Processing , pages 317 -- 325 . IEEE, 1992 . P.B. Gibbons and E. Korach. The complexity of sequential consistency. In Parallel and Distributed Processing, pages 317--325. IEEE, 1992."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_32"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640106"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504186"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/215399.215413"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_46"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00337-4"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_3_2_1_26_1","volume-title":"The SPARC Architecture Manual Version 9","author":"Weaver D.","year":"1994","unstructured":"D. Weaver and T. Germond , editors . The SPARC Architecture Manual Version 9 . PTR Prentice Hall , 1994 . D. Weaver and T. Germond, editors. The SPARC Architecture Manual Version 9. PTR Prentice Hall, 1994."},{"key":"e_1_3_2_1_27_1","first-page":"10","article-title":"Nemos: A framework for axiomatic and executable specifications of memory consistency models","author":"Yang Y.","year":"2004","unstructured":"Y. Yang , G. Gopalakrishnan , G. Lindstrom , and K. Slind . Nemos: A framework for axiomatic and executable specifications of memory consistency models . In IPDPS , 2004 . 10 .1109\/IPDPS.2004.1302944. Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In IPDPS, 2004. 10.1109\/IPDPS.2004.1302944.","journal-title":"IPDPS"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Madrid Spain","acronym":"POPL '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706299.1706303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:26:18Z","timestamp":1750263978000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,17]]},"references-count":25,"alternative-id":["10.1145\/1706299.1706303","10.1145\/1706299"],"URL":"https:\/\/doi.org\/10.1145\/1706299.1706303","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1707801.1706303","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,17]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}