{"ID":2876539,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.00587","arxiv_id":"2509.00587","title":"A Hoare Logic for Symmetry Properties","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}.","short_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 syn...","url_abs":"https://arxiv.org/abs/2509.00587","url_pdf":"https://arxiv.org/pdf/2509.00587v2","authors":"[\"Vaibhav Mehta\",\"Justin Hsu\"]","published":"2025-08-30T18:46:28Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}