{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:23:53Z","timestamp":1760059433021,"version":"build-2065373602"},"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>\n            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\n            <jats:italic toggle=\"yes\">SymVerif<\/jats:italic>\n            , 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].\n          <\/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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8953-7060","authenticated-orcid":false,"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_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_2_1_2_1","volume-title":"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_2_1_3_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_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages (POPL) Venice Italy. 14\u201325. https:\/\/doi.org\/10.1145\/964001.964003 10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"volume-title":"International Conference on Computer Aided Verification (CAV)","author":"Clarke Edmund M.","key":"e_1_2_1_5_1","unstructured":"Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. 1998. Symmetry reductions in model checking. In International Conference on Computer Aided Verification (CAV), Vancouver, British Columbia. 147\u2013158."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_18"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010178"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2003.1251058"},{"volume-title":"Presentations of Groups (2 ed.)","author":"Johnson D. L.","key":"e_1_2_1_11_1","unstructured":"D. L. Johnson. 1997. Presentations of Groups (2 ed.). Cambridge University Press."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_43"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492902000053"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Vaibhav Mehta. 2025. A Hoare Logic For Symmetry Properties. https:\/\/doi.org\/10.5281\/zenodo.16921665 10.5281\/zenodo.16921665","DOI":"10.5281\/zenodo.16921665"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"volume-title":"Nominal sets: Names and symmetry in computer science","author":"Pitts Andrew M.","key":"e_1_2_1_16_1","unstructured":"Andrew M. Pitts. 2013. Nominal sets: Names and symmetry in computer science. Cambridge University Press."},{"volume-title":"An introduction to the theory of groups. 148","author":"Rotman Joseph J.","key":"e_1_2_1_17_1","unstructured":"Joseph J. Rotman. 2012. An introduction to the theory of groups. 148, Springer-Verlag."},{"volume-title":"Automated Technology for Verification and Analysis (ATVA), Taipei City, Taiwan","author":"Sibai Hussein","key":"e_1_2_1_18_1","unstructured":"Hussein Sibai, Navid Mokhlesi, and Sayan Mitra. 2019. Using Symmetry Transformations in Equivariant Dynamical Systems for Their Safety Verification. In Automated Technology for Verification and Analysis (ATVA), Taipei City, Taiwan. Springer-Verlag, 98\u2013114. isbn:978-3-030-31784-3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_1_21_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":[[2025,10,9]],"date-time":"2025-10-09T17:50:35Z","timestamp":1760032235000},"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}