{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:20:53Z","timestamp":1770247253426,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["N66001-21-C-4028"],"award-info":[{"award-number":["N66001-21-C-4028"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["RS-2022-00165647"],"award-info":[{"award-number":["RS-2022-00165647"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>This paper studies an extension of O\u2019Hearn\u2019s incorrectness logic (IL) that allows backwards reasoning. IL in its current form does not generically permit backwards reasoning. We show t at this can be mitigated by extending IL with underspecification. The resulting logic combines underspecification (the result, or postcondition, only needs to formulate constraints over relevant variables) with underapproximation (it allows to focus on fewer than all the paths). We prove soundness of the proof system, as well as completeness for a defined subset of presumptions. We discuss proof strategies that allow one to derive a presumption from a given result. Notably, we show that the existing concept of loop summaries- closed-form symbolic representations that summarize the effects of executing an entire loop at once- is highly useful. The logic, the proof system and all theorems have been formalized in the Isabelle\/HOL theorem prover.<\/jats:p>","DOI":"10.1145\/3704850","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"391-415","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On Extending Incorrectness Logic with Backwards Reasoning"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6625-1123","authenticated-orcid":false,"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Open Universiteit of the Netherlands, Heerlen, Netherlands"},{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4318-4850","authenticated-orcid":false,"given":"Md Syadus","family":"Sefat","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2073-0564","authenticated-orcid":false,"given":"Zhoulai","family":"Fu","sequence":"additional","affiliation":[{"name":"State University of New York, Incheon, Republic of Korea"},{"name":"Stony Brook University, New York, USA"},{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8663-739X","authenticated-orcid":false,"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"[n. d.]. LibFuzzer - a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html. Accessed: 2024-01."},{"key":"e_1_3_2_3_2","article-title":"Sufficient Incorrectness Logic: SIL and Separation SIL","author":"Ascari Flavio","year":"2023","unstructured":"Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2023. Sufficient Incorrectness Logic: SIL and Separation SIL. arXiv preprint arXiv:2310.18156 (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.18156 10.48550\/arXiv.2310.18156","journal-title":"arXiv preprint arXiv:2310.18156"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","unstructured":"Roberto Baldoni Emilio Coppa Daniele Cono D'elia Camil Demetrescu and Irene Finocchi. 2018. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR) 51 3 (2018) 1\u201339. https:\/\/doi.org\/10.1145\/3182657 10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_5_2","first-page":"1","volume-title":"International Symposium on Formal Methods for Components and Objects","author":"Ball Thomas","year":"2004","unstructured":"Thomas Ball. 2004. A theory of predicate-complete test coverage and generation. In International Symposium on Formal Methods for Components and Objects. Springer, 1\u201322. https:\/\/doi.org\/10.1007\/11561163_1 10.1007\/11561163_1"},{"key":"e_1_3_2_6_2","first-page":"34","volume-title":"International Workshop on Types for Proofs and Programs","author":"Ballarin Clemens","year":"2003","unstructured":"Clemens Ballarin. 2003. Locales and locale expressions in Isabelle\/Isar. In International Workshop on Types for Proofs and Programs. Springer, 34\u201350. https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3 10.1007\/978-3-540-24849-1_3"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_2_8_2","unstructured":"Cristian Cadar Daniel Dunbar Dawson R Engler et al. 2008. KLEE: unassisted and automatic generation of high- coverage tests for complex systems programs. In OSDI Vol.8. 209-224. https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756 10.5555\/1855741.1855756"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Edmund M Clarke E Allen Emerson and A Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS) 8 2 (1986) 244\u2013263. https:\/\/dl.acm.org\/doi\/10.1145\/5397.5399 10.1145\/5397.5399","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.005"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_3_2_22_2","unstructured":"Stephen Cole Kleene. 1952. Introduction to Metamathematics. P. Noordhoff N.V. Groningen."},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Quang Loc Le Azalea Raad Jules Villard Josh Berdine Derek Dreyer and Peter W O'Hearn. 2022. Finding real bugs in big programs with incorrectness logic. Proceedings of the ACM on Programming Languages 6 OOPSLA1 (2022) 1\u201327. https:\/\/doi.org\/10.5281\/zenodo.6342311 10.5281\/zenodo.6342311","DOI":"10.1145\/3527325"},{"key":"e_1_3_2_24_2","unstructured":"James Li Noam Zilberstein and Alexandra Silva. 2024. Total Outcome Logic: Proving Termination and Nontermination in Programs with Branching. arXivpreprintarXiv:2411.00197 (2024). https:\/\/doi.org\/10.48550\/arXiv.2411.00197 10.48550\/arXiv.2411.00197"},{"key":"e_1_3_2_25_2","unstructured":"Petar Maksimovic Caroline Cronjager Andreas Loow Julian Sutherland and Philippa Gardner. 2023. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). 19:1\u201319:27. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2023.19 10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Bernhard Moller Peter O'Hearn and Tony Hoare. 2021. On algebra of program correctness and incorrectness. In Relational and Algebraic Methods in Computer Science: 19th International Conference RAMiCS 2021 Marseille France November 2-5 2021 Proceedings 19. Springer 325\u2013343. https:\/\/doi.org\/10.1007\/978-3-030-88701-8_20 10.1007\/978-3-030-88701-8_20","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"Peter W O'Hearn. 2019. Incorrectness logic. Proceedings of the ACM on Programming Languages 4 POPL (2019) 1\u201332. https:\/\/doi.org\/10.1145\/3371078 10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572299"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/SecDev.2016.043"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336772"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_19"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950340"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771815"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_3_2_39_2","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\/3704850","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704850","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:52Z","timestamp":1770200152000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704850"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704850"],"URL":"https:\/\/doi.org\/10.1145\/3704850","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}