An Abstract Domain for Heap Commutativity
Commutativity of program code (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 recent works 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.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | Abstract Local Completeness: A Local form of Abstract Non-Interference VMCAI 2025 Isabella Mastroeni University of Verona | ||
14:30 30mTalk | An Abstract Domain for Heap Commutativity VMCAI 2025 | ||
15:00 30mTalk | Two-way collaboration between flow and proof in SPARK VMCAI 2025 |