P³: reasoning about patches via product programs
File(s)
Published version
Author(s)
Sharma, Arindam
Schemmel, Daniel
Cadar, Cristian
Type
Journal Article
Abstract
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., “the post-patch version is a refactoring of the pre-patch one”) is often easy. To reason about such specifications, program analysers have to concomitantly analyse the pre- and post-patch software versions.
In this paper, we propose P3, a framework for automated reasoning about patches via product programs. While product programs have been used before, particularly in a security context, P3 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 P3 can successfully handle intricate code, inter-operate with the widely-used analysers AFL++ and KLEE, and enable reasoning over patch specifications.
In this paper, we propose P3, a framework for automated reasoning about patches via product programs. While product programs have been used before, particularly in a security context, P3 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 P3 can successfully handle intricate code, inter-operate with the widely-used analysers AFL++ and KLEE, and enable reasoning over patch specifications.
Date Issued
2025-10-01
Date Acceptance
2025-08-12
Citation
Proceedings of the ACM on Programming Languages, 2025, 9 (OOPSLA2), pp.2654-2680
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
2654
End Page
2680
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
9
Issue
OOPSLA2
Copyright Statement
© 2025 Owner/Author. This work is licensed under Creative Commons Attribution International 4.0.
License URL
Publication Status
Published
Article Number
367
Date Publish Online
2025-03-25