{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:24:03Z","timestamp":1776317043984,"version":"3.50.1"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,3,25]],"date-time":"2023-03-25T00:00:00Z","timestamp":1679702400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Italian MIUR","award":["201784YSZ5"],"award-info":[{"award-number":["201784YSZ5"]}]},{"name":"Facebook Research"},{"name":"Amazon Research Award"},{"name":"WhatsApp Research Award"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2023,4,30]]},"abstract":"<jats:p>\n            Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called\n            <jats:italic>local completeness<\/jats:italic>\n            , which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain\n            <jats:italic>A<\/jats:italic>\n            , for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain\n            <jats:italic>A<\/jats:italic>\n            , combines over- and under-approximating reasoning. In a provable triple \u22a6\n            <jats:sub>\n              <jats:italic>A<\/jats:italic>\n            <\/jats:sub>\n            [\n            <jats:italic>p<\/jats:italic>\n            ] \ud835\uddbc [\n            <jats:italic>q<\/jats:italic>\n            ], \ud835\uddbc is a program,\n            <jats:italic>q<\/jats:italic>\n            is an under-approximation of the strongest post-condition of \ud835\uddbc on input\n            <jats:italic>p<\/jats:italic>\n            such that their abstractions in\n            <jats:italic>A<\/jats:italic>\n            coincide. This means that\n            <jats:italic>q<\/jats:italic>\n            is never too coarse, namely, under some mild assumptions,\n            <jats:italic>\n              the abstract interpretation of \ud835\uddbc does not yield false alarms for the input\n              <jats:italic>p<\/jats:italic>\n              iff\n              <jats:italic>q<\/jats:italic>\n              has no alarm\n            <\/jats:italic>\n            . Therefore, proving \u22a6\n            <jats:sub>\n              <jats:italic>A<\/jats:italic>\n            <\/jats:sub>\n            [\n            <jats:italic>p<\/jats:italic>\n            ] \ud835\uddbc [\n            <jats:italic>q<\/jats:italic>\n            ] not only ensures that all the alarms raised in\n            <jats:italic>q<\/jats:italic>\n            are true ones, but also that if\n            <jats:italic>q<\/jats:italic>\n            does not raise alarms, then \ud835\uddbc is correct. We also prove that if\n            <jats:italic>A<\/jats:italic>\n            is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O\u2019Hearn\u2019s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.\n          <\/jats:p>","DOI":"10.1145\/3582267","type":"journal-article","created":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T14:01:15Z","timestamp":1675692075000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["A Correctness and Incorrectness Program Logic"],"prefix":"10.1145","volume":"70","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"first","affiliation":[{"name":"University of Pisa, Pisa, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9582-3960","authenticated-orcid":false,"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, 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\/0000-0003-0159-0068","authenticated-orcid":false,"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[{"name":"University of Padova, Padova, Italy"}]}],"member":"320","published-online":{"date-parts":[[2023,3,25]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_2"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057391"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155095"},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371096"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523453"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_3_9_1","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press."},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_8"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_3_15_1","first-page":"1","volume-title":"Chapter I: Notes on Structured Programming","author":"Dijkstra Edsger W.","year":"1972","unstructured":"Edsger W. Dijkstra. 1972a. Chapter I: Notes on Structured Programming. Academic Press Ltd., GBR, 1\u201382."},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/355604.361591"},{"key":"e_1_3_3_17_1","article-title":"Turing Award Lecture","author":"Dijkstra Edsger W.","year":"1972","unstructured":"Edsger W. Dijkstra. 1972c. Turing Award Lecture. Retrieved from https:\/\/www.youtube.com\/watch?v=6sIlKP2LzbA.","journal-title":"https:\/\/www.youtube.com\/watch?v=6sIlKP2LzbA"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234742"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_34"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0000474"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00034-8"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2021.3133136"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055786"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.145"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_3_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_3_35_1","unstructured":"Petar Maksimovic Caroline Cronj\u00e4ger Julian Sutherland Andreas L\u00f6\u00f6w Sacha-\u00c9lie Ayoun and Philippa Gardner. 2022. Exact separation logic. DOI:arXiv.2208.07200. Retrieved from https:\/\/arxiv.org\/abs\/2208.07200."},{"key":"e_1_3_3_36_1","first-page":"21","volume-title":"IFIP Congress","author":"McCarthy John","year":"1962","unstructured":"John McCarthy. 1962. Towards a mathematical science of computation. In IFIP Congress. 21\u201328."},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_16"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_3_39_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_3_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.069"},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_3_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_3_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78946-6_5"},{"key":"e_1_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100825"},{"key":"e_1_3_3_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.30"},{"key":"e_1_3_3_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_3_52_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_3_53_1","volume-title":"Introduction to Static Analysis\u2014An Abstract Interpretation Perspective","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwang Yi. 2020. Introduction to Static Analysis\u2014An Abstract Interpretation Perspective. MIT Press."},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/94938.94952"},{"key":"e_1_3_3_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"},{"key":"e_1_3_3_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_3_3_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"e_1_3_3_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498690"},{"key":"e_1_3_3_60_1","article-title":"Outcome logic: A unifying foundation for correctness and incorrectness reasoning","author":"Zilberstein Noam","year":"2023","unstructured":"Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201923), To appear.","journal-title":"Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201923)"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3582267","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3582267","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:32Z","timestamp":1750182692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3582267"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,25]]},"references-count":59,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3582267"],"URL":"https:\/\/doi.org\/10.1145\/3582267","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,25]]},"assertion":[{"value":"2022-01-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-04","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}