Verifying, Inferring and Exploiting Code Commutativity
summary
Describes automated reasoning about when two code fragments commute (C1;C2 = C2;C1), the challenges that make commutativity hard for standard relational techniques like alignment, and recent progress on verifying and synthesizing commutativity conditions. Covers applications such as enabling parallelism by embedding synthesized commutativity conditions into programming languages and outlines remaining research directions.
AI-written summary · about
related talks
58mA New Perspective on Commutativity in Verification
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
27mC4: verified transactional objects
25mUniversal Composability is Secure Compilation
40mRelational Reasoning in Object-based Programs
28mReasoning about Distributed Reconfigurable Systems
01h 05mVerifying Infinitely Many Programs at Once
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach