TY - GEN
T1 - An Abstract Domain for Heap Commutativity
AU - Pincus, Jared
AU - Koskinen, Eric
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.
PY - 2025
Y1 - 2025
N2 - Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.
AB - Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.
KW - Abstract Interpretation
KW - Commutativity
KW - Observational Equivalence
KW - Separation Logic
UR - http://www.scopus.com/inward/record.url?scp=85218439472&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85218439472&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-82703-7_2
DO - 10.1007/978-3-031-82703-7_2
M3 - Conference contribution
AN - SCOPUS:85218439472
SN - 9783031827020
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 26
EP - 49
BT - Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Proceedings
A2 - Shankaranarayanan, Krishna
A2 - Sankaranarayanan, Sriram
A2 - Trivedi, Ashutosh
T2 - 26th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2025
Y2 - 20 January 2025 through 21 January 2025
ER -