Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
summary
Graphs become a partial commutative monoid so they support join-based decomposition; structure-preserving PCM morphisms distribute over joins and let proofs localize at the mathematical level instead of the heap. The method verifies Schorr-Waite and union-find with concise mechanized proofs — 110 lines of Rock for Schorr-Waite and 49 for union-find — and ships reusable artifacts (DOI:10.1145/3747510, Zenodo:10.5281/zenodo.15847649) and a general graph PCM library.
AI-written summary · about
chapters (13)
- 0:00Separation logic for graphs
- 3:12Verifying graph algorithms challenges
- 5:19Graphs as partial monoids
- 7:05PCM morphisms for reasoning
- 10:15Proof example with morphisms
- 13:30Shortest path marking algorithm
- 16:19Conclusions and results
- 17:30Q&A: Separation logic frameworks
- 18:34Q&A: Reusing graph libraries
- 19:57Q&A: Graph properties with morphisms
- 20:40Q&A: Spatial vs nonspatial levels
- 21:44Q&A: Trees and localized reasoning
- 22:47Q&A summary
related talks
18mOn the Verification of a Subgraph Construction Algorithm
26mOn Algebraic Abstractions for Concurrent Separation Logics
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...
22mImplementing separation logic using an SMT-backed Frame Rule
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
58mA New Perspective on Commutativity in Verification
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs