Symmetric Proofs of Parameterized Programs

TL;DR

This paper introduces a new proof system leveraging symmetry to verify safety properties of infinite-state parameterized programs, enabling reuse of proof arguments and potential decision procedures.

Contribution

It proposes parametric proof spaces exploiting symmetry, provides a completeness result, and offers an algorithmic construction method for proofs in parameterized programs.

Findings

Proof system exploits symmetry for proof reuse.

Sound and complete verification method inspired by model theory.

Conditions identified for the algorithm to be a decision procedure.

Abstract

We investigate the problem of safety verification of infinite-state parameterized programs that are formed based on a rich class of topologies. We introduce a new proof system, called parametric proof spaces, which exploits the underlying symmetry in such programs. This is a local notion of symmetry which enables the proof system to reuse proof arguments for isomorphic neighbourhoods in program topologies. We prove a sophisticated relative completeness result for the proof system with respect to a class of universally quantified invariants. We also investigate the problem of algorithmic construction of these proofs. We present a construction, inspired by classic results in model theory, where an infinitary limit program can be soundly and completely verified in place of the parameterized family, under some conditions. Furthermore, we demonstrate how these proofs can be constructed and checked against these programs without the need for axiomatization of the underlying topology for proofs or the programs. Finally, we present conditions under which our algorithm becomes a decision procedure.