标题： 在分离逻辑中验证图算法：代数方法的案例（扩展版本） 显示英文标题

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

摘要： 验证图算法在分离逻辑中一直被认为具有挑战性，主要是由于图子组件之间的结构共享。 我们表明，通过将图表示为部分交换独异幂等半群（PCM），并利用保持结构的函数（PCM同态），包括高阶组合器，可以有效地解决这些挑战。 PCM同态很重要，因为它们推广了分离逻辑中的局部推理原则。 虽然传统的框架仅在规范的顶层隔离堆的相关部分，但同态允许上下文定位：它们在独异幂等半群操作上分布，以隔离相关子图，即使嵌套在规范的深层中。 我们通过两个经典图基准的新颖且简洁的验证来展示同态的有效性：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.