计算机科学 > 计算机科学中的逻辑
[提交于 2025年1月23日
(v1)
,最后修订 2025年7月9日 (此版本, v2)]
标题: 在分离逻辑中验证图算法:代数方法的案例(扩展版本)
标题: Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
摘要: 验证图算法在分离逻辑中一直被认为具有挑战性,主要是由于图子组件之间的结构共享。 我们表明,通过将图表示为部分交换独异幂等半群(PCM),并利用保持结构的函数(PCM同态),包括高阶组合器,可以有效地解决这些挑战。 PCM同态很重要,因为它们推广了分离逻辑中的局部推理原则。 虽然传统的框架仅在规范的顶层隔离堆的相关部分,但同态允许上下文定位:它们在独异幂等半群操作上分布,以隔离相关子图,即使嵌套在规范的深层中。 我们通过两个经典图基准的新颖且简洁的验证来展示同态的有效性:Schorr-Waite图标记算法和并查集数据结构。
文献和引用工具
与本文相关的代码,数据和媒体
alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)
演示
推荐器和搜索工具
arXivLabs:与社区合作伙伴的实验项目
arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。
与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。
有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.