{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:36:26Z","timestamp":1750221386984,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,4,9]],"date-time":"2018-04-09T00:00:00Z","timestamp":1523232000000},"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":[[2018,4,9]]},"DOI":"10.1145\/3167132.3167333","type":"proceedings-article","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:54:10Z","timestamp":1530626050000},"page":"1881-1890","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified compilation of linearizable data structures"],"prefix":"10.1145","author":[{"given":"Yannick","family":"Zakowski","sequence":"first","affiliation":[{"name":"Univ Rennes"}]},{"given":"David","family":"Cachera","sequence":"additional","affiliation":[{"name":"Univ Rennes"}]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[{"name":"Univ Rennes"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"Univ Rennes"}]}],"member":"320","published-online":{"date-parts":[[2018,4,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1572724.1572727"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890001"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/362422.362484"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"volume-title":"Proc. of ESOP.","author":"Feng X.","key":"e_1_3_2_1_5_1"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738006"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735844"},{"volume-title":"Mechanical verification of a garbage collector","author":"Havelund Klaus","key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0098007"},{"key":"e_1_3_2_1_10_1","unstructured":"Klaus Havelund and Natarajan Shankar. 1997. A Mechanized Refinement Proof for a Garbage Collector. (1997). Unpublished report available at http:\/\/havelund.com\/Publications\/gc-paper.ps.  Klaus Havelund and Natarajan Shankar. 1997. A Mechanized Refinement Proof for a Garbage Collector. (1997). Unpublished report available at http:\/\/havelund.com\/Publications\/gc-paper.ps."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480935"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512429.512449"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_2_1_15_1","unstructured":"M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc. San Francisco CA USA.   M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc. San Francisco CA USA."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601339"},{"key":"e_1_3_2_1_18_1","unstructured":"C. B.Jones. 1983. Specification and design of (parallel) programs. In IFIP.  C. B.Jones. 1983. Specification and design of (parallel) programs. In IFIP."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"volume-title":"Proc. of SSS'17","author":"K\u00e4stner D.","key":"e_1_3_2_1_20_1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"volume-title":"A mechanically verified incremental garbage collector. Formal Aspects of Computing 6, 4","year":"1994","author":"Russinoff David M.","key":"e_1_3_2_1_25_1"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"volume-title":"Systems Programming: Coping with Parallelism.","year":"1986","author":"Treiber R. K.","key":"e_1_3_2_1_27_1"},{"volume-title":"Proc. of CONCUR.","author":"Vafeiadis V.","key":"e_1_3_2_1_29_1"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Yannick Zakowski and David Cachera and Delphine Demange and David Pichardie. 2017. Verified Compilation of Linearizable Data Structures - Formal Development. (2017). http:\/\/www.irisa.fr\/celtique\/ext\/simulin\/.  Yannick Zakowski and David Cachera and Delphine Demange and David Pichardie. 2017. Verified Compilation of Linearizable Data Structures - Formal Development. (2017). http:\/\/www.irisa.fr\/celtique\/ext\/simulin\/.","DOI":"10.1145\/3167132.3167333"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_31"}],"event":{"name":"SAC 2018: Symposium on Applied Computing","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"],"location":"Pau France","acronym":"SAC 2018"},"container-title":["Proceedings of the 33rd Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167132.3167333","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167132.3167333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:27:00Z","timestamp":1750213620000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167132.3167333"}},"subtitle":["mechanizing rely guarantee for semantic refinement"],"short-title":[],"issued":{"date-parts":[[2018,4,9]]},"references-count":30,"alternative-id":["10.1145\/3167132.3167333","10.1145\/3167132"],"URL":"https:\/\/doi.org\/10.1145\/3167132.3167333","relation":{},"subject":[],"published":{"date-parts":[[2018,4,9]]},"assertion":[{"value":"2018-04-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}