{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:53Z","timestamp":1767929633873,"version":"3.49.0"},"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\/"}],"funder":[{"name":"Italian Ministero dell'Universit\uc3a0 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.\n \n \n \n \n \n \n \nIn contrast, under-approximation methods focus on bug detection and are free from false alarms.\n \n \n \n \n \n \n \nIn 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.\n \n \n \n \n \n \n \nThe 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.\n \n \n \n \n \n \n \nMore 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. \n \n \n \n \n \n \n \nThe 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":2,"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[{"name":"University of Pisa, Pisa, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7424-9576","authenticated-orcid":false,"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[{"name":"University of Pisa, Pisa, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4348-322X","authenticated-orcid":false,"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[{"name":"Meta Platforms, Seattle, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90066-X"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-019-00501-3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470569"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_18"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18170-9_151"},{"key":"e_1_2_1_10_1","volume-title":"Current Trends in Theoretical Computer Science, Entering the 21th Century, Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa (Eds.). World Scientific, 409\u2013436.","author":"Blass Andreas","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_2_1_11_1","volume-title":"Pysa: An Open Source Static Analysis Tool to Detect and Prevent Security Issues in Python Code. https:\/\/engineering.fb.com\/2021\/09\/29\/security\/mariana-trench\/","author":"Bleaney Graham","year":"2019","unstructured":"Graham Bleaney and Sinan Cepel. 2019. Pysa: An Open Source Static Analysis Tool to Detect and Prevent Security Issues in Python Code. https:\/\/engineering.fb.com\/2021\/09\/29\/security\/mariana-trench\/"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632849"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods Gilles Barthe Alberto Pardo and Gerardo Schneider (Eds.). Springer Berlin Heidelberg 155\u2013171. isbn:978-3-642-24690-6 https:\/\/doi.org\/10.1007\/978-3-642-24690-6_12 10.1007\/978-3-642-24690-6_12","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_26_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_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070546"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563317"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.19"},{"key":"e_1_2_1_35_1","volume-title":"Mathematical Theory of Computation","author":"Manna Zohar","unstructured":"Zohar Manna. 1974. Mathematical Theory of Computation (4th ed. ed.). McGraw-Hill. isbn:9780070399105","edition":"4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2023.25"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689720"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704850"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704896"},{"key":"e_1_2_1_46_1","volume-title":"The Formal Semantics of Programming Languages: an Introduction","author":"Winskel G.","unstructured":"G. Winskel. 1993. The Formal Semantics of Programming Languages: an Introduction. MIT press."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527331"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689740"},{"key":"e_1_2_1_49_1","unstructured":"Noam Zilberstein. 2024. A Relatively Complete Program Logic for Effectful Branching. arxiv:2401.04594. Preprint"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_2_1_51_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":[[2025,10,9]],"date-time":"2025-10-09T17:08:57Z","timestamp":1760029737000},"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"}}]}}