Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908441394544640 |
|---|---|
| author | Grandury, Marcos Nanevski, Aleksandar Gryzlov, Alexander |
| author_facet | Grandury, Marcos Nanevski, Aleksandar Gryzlov, Alexander |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_13603 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version) Grandury, Marcos Nanevski, Aleksandar Gryzlov, Alexander Logic in Computer Science Programming Languages 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. |
| title | Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2501.13603 |