An Abstract Domain for Heap Commutativity

This video presents a research talk from the VMCAI 2025 conference on "An Abstract Domain for Heap Commutativity" by Jared Pincus from Boston University and Eric Koskinen from Stevens Institute of Technology. Explore how the researchers tackle the challenge of analyzing commutativity in heap-manipulating programs through a novel abstract domain approach. Learn about their method that allows commutativity synthesis and verification to be performed on abstract mathematical models, with results that can be directly applied to concrete heap programs. The presentation demonstrates how this approach simplifies complex heap reasoning by moving it to an abstract space, while supporting important properties like framing and composition. See practical applications through commutativity analysis of programs operating on example heap data structures. The research has been mechanized in Coq and is available as a supplement. This 27-minute talk was presented at the VMCAI conference (January 20-21, 2025) and sponsored by ACM SIGPLAN.