Complete Local Reasoning About Parameterized Programs Over Topologies
2026-05-14 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors study how to automatically check if complex programs running on unlimited numbers of connected parts are safe. They focus on programs where these parts communicate over various network shapes. They show that if the network follows certain rules, you can verify the whole system by checking smaller local pieces instead of everything at once. They created a tool that uses this idea and tested it on examples, showing it helps prove program safety effectively.
parameterized programsinfinite-state systemsconcurrent programsalgorithmic verificationinductive invariantscommunication topologiescompositional verificationsafety verificationmodel checking
Authors
Ruotong Cheng, Azadeh Farzan
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.