Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Symmetric Proofs of Parameterized Programs

Ruotong Cheng, Azadeh Farzan

TL;DR

This work addresses safety verification for infinite-state, parameterized programs defined over a wide class of topologies. It introduces parametric proof spaces that exploit a local symmetry among neighbourhoods, achieving relative completeness with respect to universally quantified invariants and enabling finite, automated reasoning via limit programs and topology-aware predicate automata. The authors generalize Ashcroft invariants to a broader topology family, establish conditions for a finite basis, and show how subprograms can patch topologies to satisfy these conditions. They also develop algorithmic frameworks using limit programs and parametric predicate automata, obtaining decidability results for parameterized Boolean programs on certain topology families and providing a principled approach to verification without axiomatizing the topology. Overall, the framework enables sound, complete, and potentially decidable verification for rich classes of parameterized programs by combining locality-based symmetry, invariant-based reasoning, and automata-theoretic techniques.

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.

Symmetric Proofs of Parameterized Programs

TL;DR

This work addresses safety verification for infinite-state, parameterized programs defined over a wide class of topologies. It introduces parametric proof spaces that exploit a local symmetry among neighbourhoods, achieving relative completeness with respect to universally quantified invariants and enabling finite, automated reasoning via limit programs and topology-aware predicate automata. The authors generalize Ashcroft invariants to a broader topology family, establish conditions for a finite basis, and show how subprograms can patch topologies to satisfy these conditions. They also develop algorithmic frameworks using limit programs and parametric predicate automata, obtaining decidability results for parameterized Boolean programs on certain topology families and providing a principled approach to verification without axiomatizing the topology. Overall, the framework enables sound, complete, and potentially decidable verification for rich classes of parameterized programs by combining locality-based symmetry, invariant-based reasoning, and automata-theoretic techniques.

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.
Paper Structure (38 sections, 51 theorems, 29 equations, 1 figure)

This paper contains 38 sections, 51 theorems, 29 equations, 1 figure.

Table of Contents

  1. Introduction
  2. An Example Decidable Topology
  3. Background
  4. Parameterized Concurrent Programs
  5. Programs over Topologies
  6. Syntactic Runs of The Program
  7. Semantics
  8. Transition Relation
  9. Safety Specifications
  10. Parameterized Programs over a Family of Topologies
  11. Parametric Proof Spaces
  12. Hoare Triples in the Universal Structure
  13. The New Symmetry Rule
  14. Parametric Proof Spaces and Their Denotation
  15. Completeness of Parametric Proof Spaces
  16. ...and 23 more sections

Key Result

Proposition 4.1

Let $\mathbb{T}$ and $\mathbb{T}'$ be two structures over the same vocabulary. For any $\vec{a} \in \mathbb{T}^d$ and $\vec{b} \in \mathbb{T}'^{d}$, there is at most one isomorphism from $N(\vec{a})$ to $N(\vec{b})$ that maps $\vec{a}$ to $\vec{b}$.

Figures (1)

  • Figure 1: Two-Phase Convolution (a,c). The topology (b).

Theorems & Definitions (100)

  • Proposition 4.1
  • Definition 4.1: Local Symmetry $\simeq$
  • Example 4.1
  • Proposition 4.2
  • Proposition 4.3
  • Definition 4.2: Parameterized Program
  • Example 4.2
  • Example 5.1: Continuation of Example \ref{['ex:ring-ls']}
  • Theorem 5.1: Soundness of S-param
  • Definition 5.1: Parametric Proof Space
  • ...and 90 more