VMCAI 2025
Mon 20 - Tue 21 January 2025 Denver, Colorado, United States
co-located with POPL 2025
Tue 21 Jan 2025 14:30 - 15:00 at Hopscotch - Abstract Interpretation # 2 Chair(s): Alexandra Silva

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 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Abstract Interpretation # 2VMCAI 2025 at Hopscotch
Chair(s): Alexandra Silva Cornell University
14:00
30m
Talk
Abstract Local Completeness: A Local form of Abstract Non-Interference
VMCAI 2025
Isabella Mastroeni University of Verona
14:30
30m
Talk
An Abstract Domain for Heap Commutativity
VMCAI 2025
Jared Pincus Boston University, Eric Koskinen Stevens Institute of Technology
15:00
30m
Talk
Two-way collaboration between flow and proof in SPARK
VMCAI 2025
Claire Dross AdaCore, Joffrey Huguet AdaCore, Johannes Kanig AdaCore
:
:
:
: