一句话：提出基于群作用的 Hoare 逻辑，用于验证命令式程序的对称性质，并实现原型工具 SymVerif 发现实际模型错误。
许多程序正确性性质可表述为对称性，但现有形式化方法对这类性质的推理支持有限。作者针对以群作用表达的广泛对称性质，设计群作用的语法与自然蕴涵关系，支持标准构造；进而提出一种 Hoare 风格逻辑，用群作用替代传统前置/后置条件断言，验证命令式程序的对称性质。作者实现原型工具 SymVerif，并在手工基准上验证对称性质。评估表明该方法可行，且工具在 McLachlan 与 Quispel [Acta Numerica 2002] 描述的动态系统模型中发现一处错误。
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 McLachlan and Quispel [Acta Numerica 2002].