Skip to main content
CenXiv.org
此网站处于试运行阶段,支持我们!
我们衷心感谢所有贡献者的支持。
贡献
赞助
cenxiv logo > cs > arXiv:2501.13603

帮助 | 高级搜索

计算机科学 > 计算机科学中的逻辑

arXiv:2501.13603 (cs)
[提交于 2025年1月23日 (v1) ,最后修订 2025年7月9日 (此版本, v2)]

标题: 在分离逻辑中验证图算法:代数方法的案例(扩展版本)

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

Authors:Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov
摘要: 验证图算法在分离逻辑中一直被认为具有挑战性,主要是由于图子组件之间的结构共享。 我们表明,通过将图表示为部分交换独异幂等半群(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.
主题: 计算机科学中的逻辑 (cs.LO) ; 编程语言 (cs.PL)
引用方式: arXiv:2501.13603 [cs.LO]
  (或者 arXiv:2501.13603v2 [cs.LO] 对于此版本)
  https://doi.org/10.48550/arXiv.2501.13603
通过 DataCite 发表的 arXiv DOI
期刊参考: Proc. ACM Program. Lang. 9, ICFP, Article 241 (August 2025)
相关 DOI: https://doi.org/10.1145/3747510
链接到相关资源的 DOI

提交历史

来自: Marcos Grandury [查看电子邮件]
[v1] 星期四, 2025 年 1 月 23 日 12:11:57 UTC (470 KB)
[v2] 星期三, 2025 年 7 月 9 日 13:04:15 UTC (413 KB)
全文链接:

获取论文:

    查看标题为《》的 PDF
  • 查看中文 PDF
  • 查看 PDF
  • HTML(实验性)
  • TeX 源代码
  • 其他格式
许可图标 查看许可
当前浏览上下文:
cs.LO
< 上一篇   |   下一篇 >
新的 | 最近的 | 2025-01
切换浏览方式为:
cs
cs.PL

参考文献与引用

  • NASA ADS
  • 谷歌学术搜索
  • 语义学者
a 导出 BibTeX 引用 加载中...

BibTeX 格式的引用

×
数据由提供:

收藏

BibSonomy logo Reddit logo

文献和引用工具

文献资源探索 (什么是资源探索?)
连接的论文 (什么是连接的论文?)
Litmaps (什么是 Litmaps?)
scite 智能引用 (什么是智能引用?)

与本文相关的代码,数据和媒体

alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)

演示

复制 (什么是复制?)
Hugging Face Spaces (什么是 Spaces?)
TXYZ.AI (什么是 TXYZ.AI?)

推荐器和搜索工具

影响之花 (什么是影响之花?)
核心推荐器 (什么是核心?)
IArxiv 推荐器 (什么是 IArxiv?)
  • 作者
  • 地点
  • 机构
  • 主题

arXivLabs:与社区合作伙伴的实验项目

arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。

与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。

有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.

这篇论文的哪些作者是支持者? | 禁用 MathJax (什么是 MathJax?)
  • 关于
  • 帮助
  • contact arXivClick here to contact arXiv 联系
  • 订阅 arXiv 邮件列表点击这里订阅 订阅
  • 版权
  • 隐私政策
  • 网络无障碍帮助
  • arXiv 运营状态
    通过...获取状态通知 email 或者 slack

京ICP备2025123034号