{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:23:50Z","timestamp":1787592230244,"version":"build-2736575974"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Amazon","award":["Research Gift"],"award-info":[{"award-number":["Research Gift"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Program verification techniques for expressive heap logics are inevitably incomplete. In this work we argue that algorithmic techniques for reasoning with expressive heap logics can be held up to a different robust theoretical standard for completeness: FO-Completeness. FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. We illustrate a set of principles to design such logics and develop the first two heap logics that have implicit heaplets and that admit FO-Complete program verification. The logics we develop are a frame logic (FL) and a separation logic (SL-FL) that has an alternate semantics inspired by frame logic. We show a verification condition generation technique that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures.<\/jats:p>","DOI":"10.1145\/3720447","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"730-758","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["FO-Complete Program Verification for Heap Logics"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6311-1467","authenticated-orcid":false,"given":"Adithya","family":"Murali","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6019-1259","authenticated-orcid":false,"given":"Hrishikesh","family":"Balakrishnan","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3871-8523","authenticated-orcid":false,"given":"Aaron","family":"Councilman","sequence":"additional","affiliation":[{"name":"University of Illinois 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 Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567763"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2485981"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_17"},{"issue":"3","key":"e_1_3_1_5_2","article-title":"Local Reasoning for Global Invariants, Part I: Region Logic","volume":"60","author":"Banerjee Anindya","year":"2013","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. http:\/\/doi.acm.org\/10.1145\/2485982","journal-title":"J. ACM"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_14"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_24"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032266.2032278"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1980.41"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2007.17"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/2040235.2040256"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2015.1018801"},{"key":"e_1_3_1_18_2","volume-title":"Mathematical Logic","author":"Ebbinghaus H.D.","year":"1996","unstructured":"H.D. Ebbinghaus, J. Flum, and W. Thomas. 1996. Mathematical Logic. Springer New York."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_18"},{"key":"e_1_3_1_20_2","volume-title":"A Mathematical Introduction to Logic","author":"Enderton H.B.","year":"2001","unstructured":"H.B. Enderton. 2001. A Mathematical Introduction to Logic. Elsevier Science. https:\/\/books.google.com\/books?id=dVncCl_EtUkC"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802187"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_11"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674653"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Adithya Murali Hrishikesh Balakrishnan Aaron Councilman and P. Madhusudan. 2025. Frame Logic Verifier Tool. https:\/\/doi.org\/10.1145\/3580445 10.1145\/3580445","DOI":"10.1145\/3580445"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622835"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3583057"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_19"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656450"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_1_54_2","volume-title":"Decision procedures for separation logic: beyond symbolic heaps","author":"Pagel Jens","year":"2020","unstructured":"Jens Pagel. 2020. Decision procedures for separation logic: beyond symbolic heaps. Ph.D. Dissertation. Wien."},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_1_62_2","first-page":"80","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Reynolds Andrew","year":"2015","unstructured":"Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In Verification, Model Checking, and Abstract Interpretation, Deepak D\u2019Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80\u201398."},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00628-w"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563306"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.2307\/2268810"},{"key":"e_1_3_1_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_35"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720447","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720447","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:53Z","timestamp":1787588993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720447"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":74,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720447"],"URL":"https:\/\/doi.org\/10.1145\/3720447","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}