A Hoare Logic for Symmetry Properties

TL;DR

This paper introduces a Hoare logic framework and a prototype tool for verifying symmetry properties in imperative programs, addressing a gap in formal methods for reasoning about symmetries expressed via group actions.

Contribution

It proposes a formal syntax and Hoare-style logic for symmetry properties, along with a prototype verification tool called SymVerif.

Findings

Successfully verified symmetry properties on benchmarks

Discovered an error in a dynamical system model

Extended formal verification methods to include group action symmetries

Abstract

Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties expressed in terms of group actions. To specify these properties, we design a syntax for group actions, supporting standard constructions and a natural notion of entailment. Then, we develop a Hoare-style logic for verifying symmetry properties of imperative programs, where group actions take the place of the typical pre- and post-condition assertions. Finally, we develop a prototype tool SymVerif, and use it to verify symmetry properties on a series of handcrafted benchmarks. Our tool uncovered an error in a model of a dynamical system described by \citet{McLachlan_Quispel_2002}.