{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:31Z","timestamp":1772498911063,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61632005"],"award-info":[{"award-number":["61632005"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Huawei Innovation Research Program"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314595","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"111-125","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Towards certified separate compilation for concurrent programs"],"prefix":"10.1145","author":[{"given":"Hanru","family":"Jiang","sequence":"first","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Hongjin","family":"Liang","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Siyang","family":"Xiao","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Junpeng","family":"Zha","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, China"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480887"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_7"},{"key":"e_1_3_2_2_3_1","first-page":"3","article-title":"How to Miscompile Programs with \"Benign","author":"Boehm Hans-Juergen","year":"2011","unstructured":"Hans-Juergen Boehm . 2011 . How to Miscompile Programs with \"Benign \" Data Races. In HotPar. 3 \u2013 3 . Hans-Juergen Boehm. 2011. How to Miscompile Programs with \"Benign\" Data Races. In HotPar. 3\u20133.","journal-title":"Data Races. In HotPar."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Boudol. 2007. Fair Cooperative Multithreading. In CONCUR. 272\u2013286.   G\u00e9rard Boudol. 2007. Fair Cooperative Multithreading. In CONCUR. 272\u2013286.","DOI":"10.1007\/978-3-540-74407-8_19"},{"key":"e_1_3_2_2_6_1","unstructured":"CompCert Developers. 2017. CompCert-3.0.1. http:\/\/compcert.inria. fr\/release\/compcert-3.0.1.tgz  CompCert Developers. 2017. CompCert-3.0.1. http:\/\/compcert.inria. fr\/release\/compcert-3.0.1.tgz"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP. 504\u2013528.   Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP. 504\u2013528.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Rodrigo Ferreira Xinyu Feng and Zhong Shao. 2010. Parameterized Memory Models and Concurrent Separation Logic. In ESOP. 267\u2013286.  Rodrigo Ferreira Xinyu Feng and Zhong Shao. 2010. Parameterized Memory Models and Concurrent Separation Logic. In ESOP. 267\u2013286.","DOI":"10.1007\/978-3-642-11957-6_15"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_2_11_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.   Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601339"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Hanru Jiang Hongjin Liang Siyang Xiao Junpeng Zha and Xinyu Feng. 2019. Towards Certified Separate Compilation for Concurrent Programs (Technical Report and Coq Implementations). https:\/\/ plax-lab.github.io\/publications\/ccc\/  Hanru Jiang Hongjin Liang Siyang Xiao Junpeng Zha and Xinyu Feng. 2019. Towards Certified Separate Compilation for Concurrent Programs (Technical Report and Coq Implementations). https:\/\/ plax-lab.github.io\/publications\/ccc\/","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250756"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806636"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Scott Owens. 2010. Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In ECOOP. 478\u2013503.   Scott Owens. 2010. Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In ECOOP. 478\u2013503.","DOI":"10.1007\/978-3-642-14107-2_23"},{"key":"e_1_3_2_2_23_1","volume-title":"Perconti and Amal Ahmed","author":"James","year":"2014","unstructured":"James T. Perconti and Amal Ahmed . 2014 . Verifying an Open Compiler Using Multi-language Semantics. In ESOP. 128\u2013148. James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In ESOP. 128\u2013148."},{"key":"e_1_3_2_2_24_1","first-page":"1","article-title":"Promising Compilation to ARMv8 POP","volume":"22","author":"Podkopaev Anton","year":"2017","unstructured":"Anton Podkopaev , Ori Lahav , and Viktor Vafeiadis . 2017 . Promising Compilation to ARMv8 POP . In ECOOP. 22 : 1 \u2013 22 :28. Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2017. Promising Compilation to ARMv8 POP. In ECOOP. 22:1\u201322:28.","journal-title":"ECOOP."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993534"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411304.1411307"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Siyang Xiao Hanru Jiang Hongjin Liang and Xinyu Feng. 2018. NonPreemptive Semantics for Data-Race-Free Programs. In ICTAC. 513\u2013 531.  Siyang Xiao Hanru Jiang Hongjin Liang and Xinyu Feng. 2018. NonPreemptive Semantics for Data-Race-Free Programs. In ICTAC. 513\u2013 531.","DOI":"10.1007\/978-3-030-02508-3_27"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941575"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314595","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314595","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314595"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":35,"alternative-id":["10.1145\/3314221.3314595","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314595","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}