Complete Local Reasoning About Parameterized Programs Over Topologies
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913129918627840 |
|---|---|
| author | Cheng, Ruotong Farzan, Azadeh |
| author_facet | Cheng, Ruotong Farzan, Azadeh |
| contents | This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of a universally quantified inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme, that is, the verification of the parameterized family is reduced to a set of local proofs, in a complete manner. We propose a verification algorithm, which is implemented as a tool, and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15143 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Complete Local Reasoning About Parameterized Programs Over Topologies Cheng, Ruotong Farzan, Azadeh Logic in Computer Science Programming Languages This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of a universally quantified inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme, that is, the verification of the parameterized family is reduced to a set of local proofs, in a complete manner. We propose a verification algorithm, which is implemented as a tool, and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe. |
| title | Complete Local Reasoning About Parameterized Programs Over Topologies |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2605.15143 |