An Abstract Domain for Heap Commutativity
summary
Defines an abstract domain that lifts sets of concrete heaps into pure mathematical values (e.g., lists) via a projection pi, uses a purview to mark wellformed heaps, encodes malformed heaps as frowny face and ambiguous merges as smiley face, and proves a Coq mechanized soundness theorem that lets abstract commutativity (functions commute on values) yield framed concrete commutativity conditions. Demonstrations include push/pop/peek on a heap stack, composition with a counter, and plans for an abstract interpreter and richer lattices of abstract values.
AI-written summary · about
chapters (15)
- 0:00Heap commutativity analysis intro
- 1:50Stack example and commutativity
- 3:58Abstract domain design
- 7:07Concrete vs abstract mapping
- 10:40Stack ops and heap semantics
- 11:44Abstract ops and pure functions
- 12:49Soundness concrete vs abstract
- 13:54Commutativity concrete vs abstract
- 15:18Sound commutativity theorem
- 16:43Theorem for stack pairs
- 18:07Disjoint heap composition
- 19:32Stack and counter structures
- 21:18Abstract domain benefits
- 22:00Future work and plans
- 23:00Q&A
related talks
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
36mThe Abstract Method, In General
52mThink Abstractly, Work Concretely
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)
58mA New Perspective on Commutativity in Verification
12mFO-Complete Program Verification for Heap Logics
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
20mOn Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs