{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:13:33Z","timestamp":1775672013348,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","funder":[{"name":"ERC","award":["101171349"],"award-info":[{"award-number":["101171349"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779110","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"339-352","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Recipe for Modular Verification of Generic Tree Traversals"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9514-1360","authenticated-orcid":false,"given":"Laila","family":"Elbeheiry","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Lukas Armborst and Marieke Huisman. 2021. Permission-Based Verification of Red-Black Trees and Their Merging. In FormaliSE@ICSE. 111\u2013123. https:\/\/doi.org\/10.1109\/FORMALISE52586.2021.00017 10.1109\/FORMALISE52586.2021.00017","DOI":"10.1109\/FORMALISE52586.2021.00017"},{"key":"e_1_3_2_1_2_1","volume-title":"IWACO","author":"B\u00edl\u1ef3 Aurel","year":"2023","unstructured":"Aurel B\u00edl\u1ef3, Jonas Hansen, Peter M\u00fcller, and Alexander J. Summers. 2023. Compositional Reasoning about Advanced Iterator Patterns in Rust. In IWACO 2023."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Laila Elbeheiry Michael Sammler Robbert Krebbers Derek Dreyer and Deepak Garg. 2025. Artifact for A Recipe for Modular Verification of Generic Tree Traversals. https:\/\/doi.org\/10.5281\/zenodo.17799204 10.5281\/zenodo.17799204","DOI":"10.5281\/zenodo.17799204"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Jean-Christophe Filli\u00e2tre. 2006. Backtracking iterators. In ML. 55\u201362. https:\/\/doi.org\/10.1145\/1159876.1159885 10.1145\/1159876.1159885","DOI":"10.1145\/1159876.1159885"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/367390.367400"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2024.19"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/6724235.V1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_24"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656398"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_15"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_24"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_21_1","volume-title":"Tools and Techniques for the Verification of Modular Stateful Code. (Outils et techniques pour la v\u00e9rification de programmes imp\u00e9ratives modulaires). Ph. D. Dissertation","author":"Parreira Pereira M\u00e1rio Jos\u00e9","year":"1980","unstructured":"M\u00e1rio Jos\u00e9 Parreira Pereira. 2018. Tools and Techniques for the Verification of Modular Stateful Code. (Outils et techniques pour la v\u00e9rification de programmes imp\u00e9ratives modulaires). Ph. D. Dissertation. University of Paris-Saclay, France. https:\/\/tel.archives-ouvertes.fr\/tel-01980343"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Fran\u00e7ois Pottier. 2017. Verifying a hash table and its iterators in higher-order separation logic. In CPP. 3\u201316. https:\/\/doi.org\/10.1145\/3018610.3018624 10.1145\/3018610.3018624","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI. 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-25803-9_8"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Qiyuan Zhao George P\u00eerlea Zhendong Ang Umang Mathur and Ilya Sergey. 2024. Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. In CPP. 45\u201359. https:\/\/doi.org\/10.1145\/3636501.3636944 10.1145\/3636501.3636944","DOI":"10.1145\/3636501.3636944"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779110","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:46Z","timestamp":1775667286000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":27,"alternative-id":["10.1145\/3779031.3779110","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779110","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}