A Hoare Logic for Symmetry Properties

Watch this 14-minute conference presentation from OOPSLA 2025 that introduces a novel Hoare-style logic for formally verifying symmetry properties in imperative programs. Learn how researchers Vaibhav Mehta and Justin Hsu from Cornell University address the gap in existing formal methods by developing a framework that uses group actions instead of traditional pre- and post-condition assertions. Discover the syntax they designed for expressing group actions, including standard constructions and entailment relations, and explore how their approach enables verification of a broad class of symmetry properties that are common in program correctness but previously difficult to formally reason about. Examine their prototype tool SymVerif and see how it successfully verified symmetry properties across handcrafted benchmarks, including the discovery of an error in a dynamical system model from McLachlan and Quispel's work in Acta Numerica 2002. Gain insights into this innovative intersection of formal verification, group theory, and program analysis that opens new possibilities for reasoning about mathematical symmetries in software systems.