{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:42:44Z","timestamp":1725799364408},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,23]],"date-time":"2015-10-23T00:00:00Z","timestamp":1445558400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1319786"],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,23]]},"DOI":"10.1145\/2814270.2814297","type":"proceedings-article","created":{"date-parts":[[2015,11,2]],"date-time":"2015-11-02T21:04:33Z","timestamp":1446498273000},"page":"20-36","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["SATCheck: SAT-directed stateless model checking for SC and TSO"],"prefix":"10.1145","author":[{"given":"Brian","family":"Demsky","sequence":"first","affiliation":[{"name":"University of California at Irvine, USA"}]},{"given":"Patrick","family":"Lam","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]}],"member":"320","published-online":{"date-parts":[[2015,10,23]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640096"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003493"},{"key":"e_1_3_2_2_6_1","volume-title":"\u201cout of thin air","author":"Boehm H.-J.","year":"2013","unstructured":"H.-J. Boehm . N3786: Prohibiting \u201cout of thin air \u201d results in C++14. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/ docs\/papers\/ 2013 \/n3786.htm, September 2013. H.-J. Boehm. N3786: Prohibiting \u201cout of thin air\u201d results in C++14. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/ docs\/papers\/2013\/n3786.htm, September 2013."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_2_2_8_1","volume-title":"\u201cout of thin air","author":"Boehm H.-J.","year":"2013","unstructured":"H.-J. Boehm \u201cout of thin air \u201d results ( LWG 2265). http:\/\/www.open-std.org\/ jtc1\/sc22\/wg21\/docs\/papers\/ 2013 \/n3710.html, August 2013. H.-J. Boehm et al. N3710: Specifying the absence of \u201cout of thin air\u201d results (LWG2265). http:\/\/www.open-std.org\/ jtc1\/sc22\/wg21\/docs\/papers\/2013\/n3710.html, August 2013."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250760"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250762"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462162"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_2_2_15_1","unstructured":"C. Flanagan and P. Godefroid. Addendum to dynamic partial-order reduction for model checking software. http:\/\/users.soe.ucsc.edu\/~cormac\/papers\/ popl05-addendum.pdf. C. Flanagan and P. Godefroid. Addendum to dynamic partial-order reduction for model checking software. http:\/\/users.soe.ucsc.edu\/~cormac\/papers\/ popl05-addendum.pdf."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_2_19_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann G. J.","year":"2003","unstructured":"G. J. Holzmann . The SPIN Model Checker: Primer and Reference Manual . Addison-Wesley Professional , 1 st edition, 2003 . G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 1st edition, 2003.","edition":"1"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1815961.1815987"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_2_23_1","volume-title":"Proceedings of the 8th Symposium on Operating Systems Design and Implementation","author":"Musuvathi M.","year":"2008","unstructured":"M. Musuvathi , S. Qadeer , P. A. Nainar , T. Ball , G. Basler , and I. Neamtiu . Finding and reproducing Heisenbugs in concurrent programs . In Proceedings of the 8th Symposium on Operating Systems Design and Implementation , 2008 . M. Musuvathi, S. Qadeer, P. A. Nainar, T. Ball, G. Basler, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation, 2008."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508256"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_11"},{"key":"e_1_3_2_2_31_1","unstructured":"A. Williams. Dekker\u2019s algorithm implementation. http:\/\/ www.justsoftwaresolutions.co.uk\/threading\/. Dec. 2012. A. Williams. Dekker\u2019s algorithm implementation. http:\/\/ www.justsoftwaresolutions.co.uk\/threading\/. Dec. 2012."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500875"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_20"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_22"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"event":{"name":"SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Pittsburgh PA USA","acronym":"SPLASH '15"},"container-title":["Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2814270.2814297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:26:06Z","timestamp":1693866366000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814270.2814297"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,23]]},"references-count":35,"alternative-id":["10.1145\/2814270.2814297","10.1145\/2814270"],"URL":"https:\/\/doi.org\/10.1145\/2814270.2814297","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2858965.2814297","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,10,23]]},"assertion":[{"value":"2015-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}