A Hoare Logic for Symmetry Properties
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914018328838144 |
|---|---|
| author | Mehta, Vaibhav Hsu, Justin |
| author_facet | Mehta, Vaibhav Hsu, Justin |
| contents | 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}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_00587 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Hoare Logic for Symmetry Properties Mehta, Vaibhav Hsu, Justin Programming Languages 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}. |
| title | A Hoare Logic for Symmetry Properties |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.00587 |