{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T09:02:15Z","timestamp":1788080535492,"version":"build-2784847793"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Separation logic\u2019s compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges\u2014many programs display<jats:italic>computational effects<\/jats:italic>and, orthogonally, static analyzers must handle<jats:italic>incorrectness<\/jats:italic>too. We present Outcome Separation Logic (OSL), a program logic that is sound for both correctness and incorrectness reasoning in programs with varying effects. OSL has a frame rule\u2014just like separation logic\u2014but uses different underlying assumptions that open up local reasoning to a larger class of properties than can be handled by any single existing logic.<\/jats:p><jats:p>Building on this foundational theory, we also define symbolic execution algorithms that use bi-abduction to derive specifications for programs with effects. This involves a new<jats:italic>tri-abduction<\/jats:italic>procedure to analyze programs whose execution branches due to effects such as nondeterministic or probabilistic choice. This work furthers the compositionality promised by separation logic by opening up the possibility for greater reuse of analysis tools across two dimensions: bug-finding vs verification in programs with varying effects.<\/jats:p>","DOI":"10.1145\/3649821","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"276-304","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6388-063X","authenticated-orcid":false,"given":"Noam","family":"Zilberstein","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6277-435X","authenticated-orcid":false,"given":"Angelina","family":"Saliling","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Flavio Ascari Roberto Bruni Roberta Gori and Francesco Logozzo. 2023. Sufficient Incorrectness Logic: SIL and Separation SIL. arxiv:2310.18156."},{"key":"e_1_2_1_2_1","volume-title":"Permutation Semantics of Separation Logic. Master\u2019s thesis","author":"Baktiev Murat","year":"2006","unstructured":"Murat Baktiev. 2006. Permutation Semantics of Separation Logic. Master\u2019s thesis. Saarland University. https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/baktiev2006.pdf"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498719"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_9_1","volume-title":"Shape Analysis for Composite Data Structures","author":"Berdine Josh","unstructured":"Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O\u2019Hearn, Thomas Wies, and Hongseok Yang. 2007. Shape Analysis for Composite Data Structures. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 178\u2013192. isbn:978-3-540-73368-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_29"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.126.2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_28"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Thibault Dardinier and Peter M\u00fcller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). https:\/\/doi.org\/10.48550\/ARXIV.2301.10037","DOI":"10.48550\/ARXIV.2301.10037"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.25"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_2_1_35_1","unstructured":"John M. Li Amal Ahmed and Steven Holtzen. 2023. Lilac: a Modal Separation Logic for Conditional Probability. arxiv:2304.01339."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_2_1_45_1","unstructured":"Azalea Raad Julien Vanegue and Peter O\u2019Hearn. 2023. Compositional Non-Termination Proving. https:\/\/www.soundandcomplete.org\/papers\/Unter.pdf"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_47_1","volume-title":"Interprocedural Shape Analysis for Recursive Programs","author":"Rinetzky Noam","unstructured":"Noam Rinetzky and Mooly Sagiv. 2001. Interprocedural Shape Analysis for Recursive Programs. In Compiler Construction, Reinhard Wilhelm (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 133\u2013149. isbn:978-3-540-45306-2"},{"key":"e_1_2_1_48_1","unstructured":"Florian Sextl Adam Rogalewicz Tom\u00e1\u0161 Vojnar and Florian Zuleger. 2023. Sound One-Phase Shape Analysis with Biabduction. arxiv:2307.06346."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.33"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_28"},{"key":"e_1_2_1_52_1","unstructured":"Noam Zilberstein. 2024. A Relatively Complete Program Logic for Effectful Branching. arxiv:2401.04594."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","unstructured":"Noam Zilberstein Angelina Saliling and Alexandra Silva. 2024. Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects (Extended Version). arxiv:2305.04842.","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\/3649821","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":54,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649821"],"URL":"https:\/\/doi.org\/10.1145\/3649821","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}