{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:09:18Z","timestamp":1784200158739,"version":"3.55.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>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].<\/jats:p>","DOI":"10.1145\/3763080","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"842-866","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Hoare Logic for Symmetry Properties"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2357-3023","authenticated-orcid":false,"given":"Vaibhav","family":"Mehta","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8953-7060","authenticated-orcid":false,"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","volume-title":"International Workshop on Satisfiability Modulo Theories","author":"Areces Carlos","year":"2013","unstructured":"Carlos Areces, David D\u00e9harbe, Pascal Fontaine, and Ezequiel Orbe. 2013. SyMT: finding symmetries in SMT formulas. In International Workshop on Satisfiability Modulo Theories, Helsinki, Finland."},{"key":"e_1_3_1_3_1","first-page":"491","volume-title":"ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Atkey Robert","year":"2014","unstructured":"Robert Atkey. 2014. From parametricity to conservation laws, via Noether\u2019s theorem. In ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California. 491\u2013502."},{"key":"e_1_3_1_4_1","volume-title":"International Workshop on Computational Social Choice (COMSOC)","author":"Beckert Bernhard","year":"2016","unstructured":"Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich. 2016. Automated verification for functional and relational properties of voting rules. In International Workshop on Computational Social Choice (COMSOC), Toulouse, France."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028741"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010178"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2003.1251058"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168410"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_43"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492902000053"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Vaibhav Mehta. 2025. A Hoare Logic For Symmetry Properties. doi:10.5281\/zenodo.16921665","DOI":"10.5281\/zenodo.16921665"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_1_18_1","volume-title":"An introduction to the theory of groups","author":"Rotman Joseph J.","year":"2012","unstructured":"Joseph J. Rotman. 2012. An introduction to the theory of groups. Vol. 148. Springer-Verlag."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_6"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.3390\/sym2020799"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763080","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:11:16Z","timestamp":1784196676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763080"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":21,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763080"],"URL":"https:\/\/doi.org\/10.1145\/3763080","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}