{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:27:44Z","timestamp":1787563664940,"version":"build-2736575974"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n                    We propose a novel mechanism of defining data structures using\n                    <jats:italic toggle=\"yes\">intrinsic definitions<\/jats:italic>\n                    that avoids recursion and instead utilizes\n                    <jats:italic toggle=\"yes\">monadic maps satisfying local conditions.<\/jats:italic>\n                    We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using B\n                    <jats:sc>oogie<\/jats:sc>\n                    and prove a suite of data structure manipulating programs correct.\n                  <\/jats:p>","DOI":"10.1145\/3656450","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T12:27:20Z","timestamp":1718886440000},"page":"1804-1829","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Predictable Verification using Intrinsic Definitions"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7824-4054","authenticated-orcid":false,"given":"Cody","family":"Rivera","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"crossref","unstructured":"Timos Antonopoulos Nikos Gorogiannis Christoph Haase Max Kanovich and Joel Ouaknine. 2014. Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In Foundations of Software Science and Computation Structures Anca Muscholl (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 411-425.","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"e_1_3_2_3_1","doi-asserted-by":"crossref","unstructured":"Anindya Banerjee Mike Barnett and David A. Naumann. 2008. Boogie Meets Regions: A Verification Experience Report. In Verified Software: Theories Tools Experiments Natarajan Shankar and Jim Woodcock (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 177-191.","DOI":"10.1007\/978-3-540-87873-5_16"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Anindya Banerjee and David A. Naumann. 2013. Local Reasoning for Global Invariants Part II: Dynamic Boundaries.J. ACM 60 3 Article 19 (jun 2013) 73 pages. https:\/\/doi.org\/10.1145\/2485981 10.1145\/2485981","DOI":"10.1145\/2485981"},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","unstructured":"Anindya Banerjee David A. Naumann and Stan Rosenberg. 2008. Regional Logic for Local Reasoning about Global Invariants. In ECOOP 2008 - Object-Oriented Programming Jan Vitek (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 387-411.","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","unstructured":"Anindya Banerjee David A. Naumann and Stan Rosenberg. 2013. Local Reasoning for Global Invariants Part I: Region Logic. J. ACM 60 3 Article 18 (June 2013) 56 pages. https:\/\/doi.org\/10.1145\/2485982 10.1145\/2485982","DOI":"10.1145\/2485982"},{"key":"e_1_3_2_7_1","doi-asserted-by":"crossref","unstructured":"Mike Barnett Bor-Yuh Evan Chang Robert DeLine Bart Jacobs and K. Rustan M. Leino. 2006. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects Frank S. de Boer Marcello M. Bonsangue Susanne Graf and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 364-387.","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_8_1","doi-asserted-by":"crossref","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovic Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 171-177.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_9_1","doi-asserted-by":"crossref","unstructured":"Josh Berdine Cristiano Calcagno and Peter W. O\u2019Hearn. 2005. A Decidable Fragment of Separation Logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science Kamal Lodaya and Meena Mahajan (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 97-109.","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Josh Berdine Cristiano Calcagno and Peter W. O\u2019Hearn. 2005. Symbolic Execution with Separation Logic. In Programming Languages and Systems Kwangkeun Yi (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 52-68.","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_12_1","doi-asserted-by":"crossref","unstructured":"Remi Brochenin Stephane Demri and Etienne Lozes. 2008. On the Almighty Wand. In Computer Science Logic Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 323-338.","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter W. O\u2019Hearn and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58 6 Article 26 (dec 2011) 66 pages. https:\/\/doi.org\/10.1145\/2049697.2049700 10.1145\/2049697.2049700","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.17"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737984"},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Ernie Cohen Markus Dahlweid Mark Hillebrand Dirk Leinenbach Michal Moskal Thomas Santen Wolfram Schulte and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics Stefan Berghofer Tobias Nipkow Christian Urban and Makarius Wenzel (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 23-42.","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Jeremy Condit Brian Hackett Shuvendu K. Lahiri and Shaz Qadeer. 2009. Unifying Type Checking and Property Checking for Low-Level Code. SIGPLANNot. 44 1 (jan 2009) 302-314. https:\/\/doi.org\/10.1145\/1594834.1480921 10.1145\/1594834.1480921","DOI":"10.1145\/1594834.1480921"},{"key":"e_1_3_2_18_1","first-page":"337","article-title":"Z3: An Efficient SMT Solver","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj0rner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS\u201908). Springer-Verlag, Berlin, Heidelberg, 337-340.","journal-title":"In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS\u201908). Springer-Verlag, Berlin, Heidelberg"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura and Nikolaj Bj0rner. 2009. Generalized efficient array decision procedures. In 2009Formal Methods in Computer-Aided Design. IEEE 45-52. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142 10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"e_1_3_2_20_1","doi-asserted-by":"crossref","unstructured":"David Dill Wolfgang Grieskamp Junkil Park Shaz Qadeer Meng Xu and Emma Zhong. 2022. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. In Tools and Algorithms for the Construction and Analysis of Systems Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing Cham 183-200.","DOI":"10.1007\/978-3-030-99524-9_10"},{"key":"e_1_3_2_21_1","doi-asserted-by":"crossref","unstructured":"Dino Distefano Peter W. O\u2019Hearn and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In Tools and Algorithms for the Construction and Analysis of Systems Holger Hermanns and Jens Palsberg (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 287-302.","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Dino Distefano and Matthew Parkinson. 2008. jStar: Towards Practical Verification for Java. Sigplan Notices - SIGPLAN 43 213-226. https:\/\/doi.org\/10.1145\/1449764.1449782 10.1145\/1449764.1449782","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_2_23_1","doi-asserted-by":"crossref","unstructured":"Mnacho Echenim Radu Iosif and Nicolas Peltier. 2021. Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In Automated Deduction - CADE 28 Andre Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing Cham 183-199.","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filliatre Leon Gondelman and Andrei Paskevich. 2016. The spirit of ghost code. Formal Methods in System Design 48 (2016) 152-174.","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Alex Gyori Pranav Garg Edgar Pek and P. Madhusudan. 2017. Efficient Incrementalized Runtime Checking of Linear Measures on Lists. In 2017 IEEE International Conference on Software Testing Verification and Validation ICST 2017 Tokyo Japan March 13-17 2017. IEEE Computer Society 310-320. https:\/\/doi.org\/10.1109\/ICST.2017.35 10.1109\/ICST.2017.35","DOI":"10.1109\/ICST.2017.35"},{"key":"e_1_3_2_26_1","doi-asserted-by":"crossref","unstructured":"Radu Iosif Adam Rogalewicz and Jiri Simacek. 2013. The Tree Width of Separation Logic with Recursive Definitions. In Automated Deduction - CADE-24 Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 21-38.","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_3_2_27_1","first-page":"41","article-title":"VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java","author":"Jacobs Bart","year":"2011","unstructured":"Bart Jacobs, Jan Smans, Pieter Philippaerts, Frederic Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In Proceedings of the Third International Conference on NASA Formal Methods (Pasadena, CA) (NFM\u201911). Springer-Verlag, Berlin, Heidelberg, 41-55.","journal-title":"In Proceedings of the Third International Conference on NASA Formal Methods (Pasadena, CA) (NFM\u201911). Springer-Verlag, Berlin, Heidelberg"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"C. B. Jones. 2010. The Role of Auxiliary Variables in the Formal Development of Concurrent Programs. In Reflections on the Work ofC.A.R. Hoare A.W. Roscoe Cliff B. Jones and Kenneth R. Wood (Eds.). Springer London London 167-187. https:\/\/doi.org\/10.1007\/978-1-84882-912-1_8 10.1007\/978-1-84882-912-1_8","DOI":"10.1007\/978-1-84882-912-1_8"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In 2021 Formal Methods in ComputerAided Design (FMCAD). 143-152. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_23 10.34727\/2021\/isbn.978-3-85448-046-4_23","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_23"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Siddharth Krishna Dennis E. Shasha and Thomas Wies. 2018. Go with the flow: compositional abstractions for concurrent data structures. Proc. ACMProgram. Lang. 2 POPL (2018) 37:1-37:31. https:\/\/doi.org\/10.1145\/3158125 10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_12"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Shuvendu Lahiri and Shaz Qadeer. 2008. Back to the Future: Revisiting Precise Program Verification Using SMT Solvers. SIGPLANNot. 43 1 (jan 2008) 171-182. https:\/\/doi.org\/10.1145\/1328897.1328461 10.1145\/1328897.1328461","DOI":"10.1145\/1328897.1328461"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Andrea Lattuada Travis Hance Chanhee Cho Matthias Brun Isitha Subasinghe Yi Zhou Jon Howell Bryan Parno and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang. 7 OOPSLA1 Article 85 (apr 2023) 30 pages. https:\/\/doi.org\/10.1145\/3586037 10.1145\/3586037","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_35_1","doi-asserted-by":"crossref","unstructured":"Oukseh Lee Hongseok Yang and Rasmus Petersen. 2011. Program Analysis for Overlaid Data Structures. In Computer Aided Verification Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 592-608.","DOI":"10.1007\/978-3-642-22110-1_48"},{"key":"e_1_3_2_36_1","doi-asserted-by":"crossref","unstructured":"K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning. Springer 348-370.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Tal Lev-Ami Neil Immerman Thomas Reps Mooly Sagiv Siddharth Srivastava and Greta Yorsh. 2009. Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5 (04 2009). https:\/\/doi.org\/10.2168\/LMCS-5(2:12)2009 10.2168\/LMCS-5(2:12)2009","DOI":"10.2168\/LMCS-5(2:12)2009"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Christof Loding P. Madhusudan and Lucas Pena. 2018. Foundations for natural proofs and quantifier instantiation. PACMPL 2 POPL (2018) 10:1-10:30. https:\/\/doi.org\/10.1145\/3158098 10.1145\/3158098","DOI":"10.1145\/3158098"},{"key":"e_1_3_2_39_1","unstructured":"P Lucas. 1968. Two constructive realizations of the block concept and their equivalence IBM Lab. Technical Report. Vienna TR 25.085."},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"P. Madhusudan Gennaro Parlato and Xiaokang Qiu. 2011. Decidable Logics Combining Heap Structures and Data. SIGPLAN Not. 46 1 (jan 2011) 611-622. https:\/\/doi.org\/10.1145\/1925844.1926455 10.1145\/1925844.1926455","DOI":"10.1145\/1925844.1926455"},{"key":"e_1_3_2_41_1","doi-asserted-by":"crossref","unstructured":"P. Madhusudan and Xiaokang Qiu. 2011. Efficient Decision Procedures for Heaps Using STRAND. In Static Analysis Eran Yahav (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 43-59.","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Roland Meyer Thomas Wies and Sebastian Wolff. 2022. A Concurrent Program Logic with a Future and History. Proc. ACM Program. Lang. 6 OOPSLA2 Article 174 (oct 2022) 30 pages. https:\/\/doi.org\/10.1145\/3563337 10.1145\/3563337","DOI":"10.1145\/3563337"},{"key":"e_1_3_2_43_1","first-page":"628","article-title":"Make Flows Small Again: Revisiting the Flow Framework","author":"Meyer Roland","year":"2023","unstructured":"Roland Meyer, Thomas Wies, and Sebastian Wolff. 2023. Make Flows Small Again: Revisiting the Flow Framework. In Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part I (Paris, France). Springer-Verlag, Berlin, Heidelberg, 628-646. https:\/\/doi.org\/10.1007\/978-3-031- 30823-9_32","journal-title":"In Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part I (Paris, France). Springer-Verlag, Berlin, Heidelberg"},{"key":"e_1_3_2_44_1","doi-asserted-by":"crossref","unstructured":"Peter Muller Malte Schwerhoff and Alexander J. Summers. 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Computer Aided Verification Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing Cham 405-425.","DOI":"10.1007\/978-3-319-41528-4_22"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Adithya Murali Lucas Pena Eion Blanchard Christof Loding and P. Madhusudan. 2022. Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints. Proc. ACM Program. Lang. 6 OOPSLA2 Article 191 (oct 2022) 30 pages. https:\/\/doi.org\/10.1145\/3563354 10.1145\/3563354","DOI":"10.1145\/3563354"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Adithya Murali Lucas Pena Ranjit Jhala and P. Madhusudan. 2023. Complete First-Order Reasoning for Properties of Functional Programs. Proc. ACM Program. Lang. 7 OOPSLA2 Article 259 (oct 2023) 30 pages. https:\/\/doi.org\/10.1145\/3622835 10.1145\/3622835","DOI":"10.1145\/3622835"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Adithya Murali Cody Rivera and P. Madhusudan. 2024. Artifact for \u201cPredictable Verification using Intrinsic Definitions\u201d (v1.0). https:\/\/doi.org\/10.5281\/zenodo.10963124 10.5281\/zenodo.10963124","DOI":"10.5281\/zenodo.10963124"},{"key":"e_1_3_2_48_1","unstructured":"Adithya Murali Cody Rivera and P. Madhusudan. 2024. Predictable Verification using Intrinsic Defintitions (Technical Report) arXiv 2404.04515. https:\/\/arxiv.org\/abs\/2404.04515"},{"key":"e_1_3_2_49_1","unstructured":"Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph.D. Dissertation. Stanford University Stanford CA USA. AAI8011683."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures. ACM Trans. Program. Lang. Syst. 1 2 (oct 1979) 245-257. https:\/\/doi.org\/10.1145\/357073.357079 10.1145\/357073.357079","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification Tobias Nipkow Orna Grumberg and Benedikt Hauptmann (Eds.). NATO Science for Peace and Security Series - D: Information and Communication Security Vol. 33. IOS Press 286-318. https:\/\/doi.org\/10.3233\/978-1-61499-028-4-286 10.3233\/978-1-61499-028-4-286","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_3_2_53_1","first-page":"1","article-title":"Local Reasoning About Programs That Alter Data Structures","author":"O\u2019Hearn Peter W.","year":"2001","unstructured":"Peter W. O\u2019Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning About Programs That Alter Data Structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL \u201801). Springer-Verlag, London, UK, UK, 1-19. http:\/\/dl.acm.org\/citation.cfm?id=647851.737404","journal-title":"In Proceedings of the 15th International Workshop on Computer Science Logic (CSL \u201801). Springer-Verlag, London, UK, UK"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","unstructured":"Nisarg Patel Siddharth Krishna Dennis Shasha and Thomas Wies. 2021. Verifying Concurrent Multicopy Search Structures. Proc. ACM Program. Lang. 5 OOPSLA Article 113 (oct 2021) 32 pages. https:\/\/doi.org\/10.1145\/3485490 10.1145\/3485490","DOI":"10.1145\/3485490"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","unstructured":"Edgar Pek Xiaokang Qiu and P. Madhusudan. 2014. Natural Proofs for Data Structure Manipulation in C Using Separation Logic. SIGPLANNot. 49 6 (jun 2014) 440-451. https:\/\/doi.org\/10.1145\/2666356.2594325 10.1145\/2666356.2594325","DOI":"10.1145\/2666356.2594325"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_3_2_57_1","first-page":"711","article-title":"Automating Separation Logic with Trees and Data","author":"Piskac Ruzica","year":"2014","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. Automating Separation Logic with Trees and Data. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201914). Springer-Verlag, Berlin, Heidelberg, 711-728.","journal-title":"In Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201914). Springer-Verlag, Berlin, Heidelberg"},{"key":"e_1_3_2_58_1","unstructured":"John C. Reynolds. 1981. The craft of programming. Prentice Hall."},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","unstructured":"Patrick M. Rondon Ming Kawaguci and Ranjit Jhala. 2008. Liquid types. SIGPLANNot. 43 6 (jun 2008) 159-169. https:\/\/doi.org\/10.1145\/1379022.1375602 10.1145\/1379022.1375602","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","unstructured":"Mooly Sagiv Thomas Reps and Reinhard Wilhelm. 2002. Parametric Shape Analysis via 3-Valued Logic. ACM Trans. Program. Lang. Syst. 24 3 (may 2002) 217-298. https:\/\/doi.org\/10.1145\/514188.514190 10.1145\/514188.514190","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","unstructured":"Quang-Trung Ta Ton Chanh Le Siau-Cheng Khoo and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof in Separation Logic. In FM 2016: Formal Methods John Fitzgerald Constance Heitmeyer Stefania Gnesi and Anna Philippou (Eds.). Springer International Publishing Cham 659-676. https:\/\/doi.org\/10.1007\/978-3-319-48989-6_40 10.1007\/978-3-319-48989-6_40","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_2_64_1","doi-asserted-by":"crossref","unstructured":"Cesare Tinelli and Calogero G. Zarba. 2004. Combining Decision Procedures for Sorted Theories. In Logics in Artificial Intelligence Jose Julio Alferes and Joao Leite (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 641-653.","DOI":"10.1007\/978-3-540-30227-8_53"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656450","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656450","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:42:51Z","timestamp":1751647371000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656450"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":63,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656450"],"URL":"https:\/\/doi.org\/10.1145\/3656450","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}