{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:04Z","timestamp":1767927904361,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"name":"Singapore Ministry of Education","award":["MOE-MOET32021-0001"],"award-info":[{"award-number":["MOE-MOET32021-0001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636944","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"45-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic"],"prefix":"10.1145","author":[{"given":"Qiyuan","family":"Zhao","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"given":"George","family":"P\u00eerlea","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"given":"Zhendong","family":"Ang","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_2_1","volume-title":"Software Foundations.","volume":"3","author":"Appel Andrew W.","year":"2016","unstructured":"Andrew W. Appel. 2016. Verified Functional Algorithms. Software Foundations., Volume 3 (2016), Available at https:\/\/softwarefoundations.cis.upenn.edu\/vfa-current\/"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel. 2022. Coq\u2019s vibrant ecosystem for verification engineering (invited talk). In CPP. ACM 2\u201311. https:\/\/doi.org\/10.1145\/3497775.3503951 10.1145\/3497775.3503951","DOI":"10.1145\/3497775.3503951"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.03.006"},{"key":"e_1_3_2_1_5_1","unstructured":"Aur\u00e8le Barri\u00e8re. 2018. VST Verification of B+ Trees with Cursors. Ecole Normale Sup\u00e9rieure de Rennes."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1909.08789"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Arthur Chargu\u00e9raud. 2016. Higher-order representation predicates in separation logic. In CPP. ACM 3\u201314. https:\/\/doi.org\/10.1145\/2854065.2854068 10.1145\/2854065.2854068","DOI":"10.1145\/2854065.2854068"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_3_2_1_9_1","volume-title":"Software Foundations.","volume":"6","author":"Chargu\u00e9raud Arthur","year":"2021","unstructured":"Arthur Chargu\u00e9raud. 2021. Separation Logic Foundations. Software Foundations., Volume 6 (2021), Available at https:\/\/softwarefoundations.cis.upenn.edu\/slf-current\/"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796822000107"},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 11th Australian Computer Science Conference. 55\u201366","author":"Fidge Colin J","year":"1988","unstructured":"Colin J Fidge. 1988. Timestamps in message-passing systems that preserve the partial ordering. In Proceedings of the 11th Australian Computer Science Conference. 55\u201366."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_2_1_13_1","volume-title":"Algebras for Tree Algorithms. Ph. D. Dissertation","author":"Gibbons Jeremy","unstructured":"Jeremy Gibbons. 1991. Algebras for Tree Algorithms. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In POPL. ACM 523\u2013536. https:\/\/doi.org\/10.1145\/2429069.2429131 10.1145\/2429069.2429131","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_3_2_1_17_1","unstructured":"The Iris Project. 2023. Iris: a Higher-Order Concurrent Separation Logic Framework implemented and verified in the Coq proof assistant. https:\/\/iris-project.org\/ Online"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Mohsen Lesani Christian J. Bell and Adam Chlipala. 2016. Chapar: certified causally consistent distributed key-value stores. In POPL. ACM 357\u2013370. https:\/\/doi.org\/10.1145\/2837614.2837622 10.1145\/2837614.2837622","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"William Mansky Yuanfeng Peng Steve Zdancewic and Joseph Devietti. 2017. Verifying dynamic race detection. In CPP. ACM 151\u2013163. https:\/\/doi.org\/10.1145\/3018610.3018611 10.1145\/3018610.3018611","DOI":"10.1145\/3018610.3018611"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507734"},{"key":"e_1_3_2_1_23_1","unstructured":"Friedemann Mattern. 1989. Virtual Time and Global States of Distributed Systems. In Parallel and Distributed Algorithms. North-Holland 215\u2013226."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_37"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Nanevski Viktor Vafeiadis and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In POPL. ACM 261\u2013274. https:\/\/doi.org\/10.1145\/1706299.1706331 10.1145\/1706299.1706331","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563351"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_29_1","unstructured":"Jos\u00e9 Nuno Oliveira. 2023. Program Design by Calculation."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_32_1","volume-title":"Workshop on Mechanizing Metatheory. 8.","author":"Sadowski Caitlin","year":"2008","unstructured":"Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, and Cormac Flanagan. 2008. Proving correctness of a dynamic atomicity analysis in Coq. In Workshop on Mechanizing Metatheory. 8."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1791194.1791203"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Ilya Sergey Aleksandar Nanevski and Anindya Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In PLDI. ACM 77\u201387. https:\/\/doi.org\/10.1145\/2737924.2737964 10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90147-A"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360597"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178514"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Qiyuan Zhao George P\u00eerlea Zhendong Ang Umang Mathur and Ilya Sergey. 2023. Artefact for Article \u201cRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic\u201d. https:\/\/doi.org\/10.5281\/zenodo.10366484 10.5281\/zenodo.10366484","DOI":"10.5281\/zenodo.10366484"}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"London UK","acronym":"CPP '24","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636944","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636944","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636944"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":38,"alternative-id":["10.1145\/3636501.3636944","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636944","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}