一句话：提出用偏交换幺半群及其态射组织图算法的分离逻辑验证，实现上下文局部推理，并简洁验证 Schorr-Waite 与并查集。
在分离逻辑中验证图算法长期困难，主要原因是图子组件之间存在结构共享，难以只隔离相关堆片段。本文提出一种代数方法：将图表示为偏交换幺半群（PCM），并利用保持结构的 PCM 态射（包括高阶组合子）进行推理。PCM 态射推广了分离逻辑的局部推理原则：传统 framing 只在规格顶层隔离相关堆部分，而态射可对幺半群运算分配，从而在规格深层嵌套时实现上下文局部化，隔离相关子图。作者以 Schorr-Waite 图标记算法和并查集两个经典基准为例，给出了新颖且简洁的验证，表明该代数方法能有效应对结构共享带来的挑战。
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.
@article{paperbot3044,
title = {Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach},
author = {Marcos Grandury and Aleksandar Nanevski and Alexander Gryzlov},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747510}
}