Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)

TL;DR

This paper introduces an algebraic approach using partial commutative monoids and morphisms to improve the verification of complex graph algorithms in separation logic, enabling modular and scalable proofs.

Contribution

It proposes representing graphs as PCM and leveraging PCM morphisms to address structural sharing challenges in separation logic verification.

Findings

Effective verification of Schorr-Waite algorithm

Concise proofs for union-find data structure

Demonstrates modular reasoning with morphisms

Abstract

Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can be effectively addressed by representing graphs as a partial commutative monoid (PCM), and by leveraging structure-preserving functions (PCM morphisms), including higher-order combinators. PCM morphisms are important because they generalize separation logic's principle of local reasoning. While traditional framing isolates relevant portions of the heap only at the top level of a specification, morphisms enable contextual localization: they distribute over monoid operations to isolate relevant subgraphs, even when nested deeply within a specification. We demonstrate the morphisms' effectiveness with novel and concise verifications of two canonical graph benchmarks: the Schorr-Waite graph marking algorithm and the union-find data structure.