{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:23:14Z","timestamp":1787592194975,"version":"build-2736575974"},"reference-count":51,"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-nc-sa\/4.0\/legalcode"}],"funder":[{"name":"Italian Ministero dell'Universit\u00e0 e della Ricerca","award":["P2022HXNSC"],"award-info":[{"award-number":["P2022HXNSC"]}]},{"name":"European Union - NextGenerationEU","award":["PE00000014 - CUP H73C2200089001"],"award-info":[{"award-number":["PE00000014 - CUP H73C2200089001"]}]},{"name":"INdAM-GNCS","award":["CUP_E53C22001930001"],"award-info":[{"award-number":["CUP_E53C22001930001"]}]},{"DOI":"10.13039\/501100007514","name":"University of Pisa","doi-asserted-by":"crossref","award":["PRA_2022_99"],"award-info":[{"award-number":["PRA_2022_99"]}],"id":[{"id":"10.13039\/501100007514","id-type":"DOI","asserted-by":"crossref"}]}],"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>Sound over-approximation methods are effective for proving the absence of errors, but inevitably produce false alarms that can hamper programmers. In contrast, under-approximation methods focus on bug detection and are free from false alarms. In this work, we present two novel proof systems designed to locate the source of errors via backward under-approximation, namely Sufficient Incorrectness Logic (SIL) and its specialization for handling memory errors, called Separation SIL. The SIL proof system is minimal, sound and complete for Lisbon triples, enabling a detailed comparison of triple-based program logics across various dimensions, including negation, approximation, execution order, and analysis objectives. More importantly, SIL lays the foundation for our main technical contribution, by distilling the inference rules of Separation SIL, a sound and (relatively) complete proof system for automated backward reasoning in programs involving pointers and dynamic memory allocation. The completeness result for Separation SIL relies on a careful crafting of both the assertion language and the rules for atomic commands.<\/jats:p>","DOI":"10.1145\/3720486","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1321-1348","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Revealing Sources of (Memory) Errors via Backward Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4624-9752","authenticated-orcid":false,"given":"Flavio","family":"Ascari","sequence":"first","affiliation":[{"name":"University of Pisa, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[{"name":"University of Pisa, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7424-9576","authenticated-orcid":false,"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[{"name":"University of Pisa, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4348-322X","authenticated-orcid":false,"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[{"name":"Meta Platforms, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90066-X"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-019-00501-3"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470569"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_18"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18170-9_151"},{"key":"e_1_3_1_11_1","first-page":"409","volume-title":"Current Trends in Theoretical Computer Science, Entering the 21th Century","author":"Blass Andreas","year":"2001","unstructured":"Andreas Blass and Yuri Gurevich. 2001. The Underlying Logic of Hoare Logic. In Current Trends in Theoretical Computer Science, Entering the 21th Century, Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa (Eds.). World Scientific, 409\u2013436."},{"key":"e_1_3_1_12_1","unstructured":"Graham Bleaney and Sinan Cepel. 2019. Pysa: An Open Source Static Analysis Tool to Detect and Prevent Security Issues in Python Code. https:\/\/engmeermg.fb.com\/2021\/09\/29\/security\/mariana-trench\/."},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632849"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_1_27_1","unstructured":"Dominik Gabi. 2021. Open-sourcing Mariana Trench: Analyzing Android and Java App Security in Depth. https:\/\/engineering.fb.com\/2021\/09\/29\/security\/mariana-trench\/."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070546"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/557365"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563317"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.19"},{"key":"e_1_3_1_36_1","volume-title":"Mathematical Theory of Computation","author":"Manna Zohar","year":"1974","unstructured":"Zohar Manna. 1974. Mathematical Theory of Computation (4th ed. ed.). McGraw-Hill.","edition":"4"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2023.25"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689720"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704850"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704896"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527331"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689740"},{"key":"e_1_3_1_50_1","unstructured":"Noam Zilberstein. 2024. A Relatively Complete Program Logic for Effectful Branching. arXiv:2401.04594 [cs.LO] Preprint."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649821"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720486","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720486","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:41Z","timestamp":1787588981000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720486"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":51,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720486"],"URL":"https:\/\/doi.org\/10.1145\/3720486","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"}}]}}