Complete Local Reasoning About Parameterized Programs Over Topologies

TL;DR

This paper presents a new compositional verification approach for infinite-state parameterized concurrent programs over various topologies, enabling automatic safety proofs through local invariants.

Contribution

It introduces a reduction of the safety verification problem to local proofs under certain topology assumptions, with an implemented algorithm demonstrating effectiveness.

Findings

Effective verification of parameterized programs over multiple topologies.

Reduction to local proofs simplifies the safety verification process.

The approach is validated on several benchmark programs.

Abstract

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.