Complete Local Reasoning About Parameterized Programs Over Topologies
For developers of concurrent systems, this provides a complete and automated method to verify safety over parameterized topologies, though the approach is domain-specific.
This work addresses the algorithmic safety verification of infinite-state parameterized concurrent programs over various communication topologies, reducing it to a complete compositional scheme of local proofs. The proposed tool effectively proves safety across multiple benchmarks and topologies.
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.