{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:19:59Z","timestamp":1760059199602,"version":"build-2065373602"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"European Research Council under the European Union?s Horizon 2020","award":["819141"],"award-info":[{"award-number":["819141"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Software systems change on a continuous basis, with each patch prone to introducing new errors and security vulnerabilities. While providing a full functional specification for the program is a notoriously difficult task, writing a patch specification that describes the behaviour of the patched version in terms of the unpatched one (e.g., \u201cthe post-patch version is a refactoring of the pre-patch one\u201d) is often easy. To reason about such specifications, program analysers have to concomitantly analyse the pre- and post-patch software versions.<\/jats:p>\n          <jats:p>\n            In this paper, we propose\n            <jats:italic toggle=\"yes\">P<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            , a framework for automated reasoning about patches via product programs. While product programs have been used before, particularly in a security context,\n            <jats:italic toggle=\"yes\">P<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            is the first framework that automatically constructs product programs for a real-world language (namely C), supports diverse and complex patches found in real software, and provides runtime support enabling techniques as varied as greybox fuzzing and symbolic execution to run unmodified. Our experimental evaluation on a set of complex software patches from the challenging CoREBench suite shows that\n            <jats:italic toggle=\"yes\">P<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            can successfully handle intricate code, inter-operate with the widely-used analysers AFL++ and KLEE, and enable reasoning over patch specifications.\n          <\/jats:p>","DOI":"10.1145\/3763145","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2654-2680","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["P\u00b3: Reasoning about Patches via Product Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5361-1057","authenticated-orcid":false,"given":"Arindam","family":"Sharma","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8769-7813","authenticated-orcid":false,"given":"Daniel","family":"Schemmel","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3599-7264","authenticated-orcid":false,"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108768.1108813"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2628058"},{"key":"e_1_2_1_6_1","volume-title":"Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE58978.2023.00012"},{"key":"e_1_2_1_8_1","unstructured":"2023. LibTooling. https:\/\/clang.llvm.org\/docs\/LibTooling.html"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/IBF50092.2020.9034714"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/362929.362947"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324783"},{"key":"e_1_2_1_12_1","volume-title":"Proc. of the 14th USENIX Workshop on Offensive Technologies (WOOT\u201920)","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi, Dominik Maier, Heiko Ei\u00df feldt, and Marc Heuse. 2020. AFL++: Combining Incremental Steps of Fuzzing Research. In Proc. of the 14th USENIX Workshop on Offensive Technologies (WOOT\u201920)."},{"key":"e_1_2_1_13_1","unstructured":"Free Software Foundation Inc. 2025. GNU Coreutils. https:\/\/www.gnu.org\/software\/coreutils\/"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3305052"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534368"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208952"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568304"},{"key":"e_1_2_1_21_1","unstructured":"LLVM. 2024. clang-diff: A Tool for Comparing Abstract Syntax Trees. https:\/\/clang.llvm.org\/ Accessed: 2024-09-08"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884872"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491438"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1525880.1525884"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST60714.2024.00036"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884845"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Arindam Sharma Daniel Schemmel and Cristian Cadar. 2025. Reproduction Package for Article \u2018P\u00b3: Reasoning about Patches via Product Programs\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.16891174 10.5281\/zenodo.16891174","DOI":"10.5281\/zenodo.16891174"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276535"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950295"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3511096"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180182"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2483760.2483772"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763145","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:42:49Z","timestamp":1760031769000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763145"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":36,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763145"],"URL":"https:\/\/doi.org\/10.1145\/3763145","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}