{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:16Z","timestamp":1780994536276,"version":"3.54.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200429"],"award-info":[{"award-number":["200429"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Algebraic laws of\n            <jats:italic toggle=\"yes\">functions in mathematics<\/jats:italic>\n            \u2013 such as commutativity, associativity, and idempotence \u2013 are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of\n            <jats:italic toggle=\"yes\">functions in coding<\/jats:italic>\n            , however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack built-in mechanisms to enforce and verify that operations adhere to such properties.\n          <\/jats:p>\n          <jats:p>In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five state-of-the-art verifiers on a total of 142 instances of algebraic properties shows that Propel is able to automatically deduce algebraic properties in different domains that rely on such properties for correctness, even in cases where competitors fail to verify the same properties or time out.<\/jats:p>","DOI":"10.1145\/3656408","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"766-789","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Automated Verification of Fundamental Algebraic Laws"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-5042-1207","authenticated-orcid":false,"given":"George","family":"Zakhour","sequence":"first","affiliation":[{"name":"University of St. Gallen, St. Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1288-1485","authenticated-orcid":false,"given":"Pascal","family":"Weisenburger","sequence":"additional","affiliation":[{"name":"University of St. Gallen, St. Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9324-8894","authenticated-orcid":false,"given":"Guido","family":"Salvaneschi","sequence":"additional","affiliation":[{"name":"University of St. Gallen, St. Gallen, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"[n.d.]. Apache Beam. https:\/\/beam.apache.org\/. Accessed: 2013-07-12."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_9"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508273"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-14805-8_4"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_7"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(94)00215-7"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/11554554_8"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_25"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032429"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_6"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Koen Claessen Moa Johansson Dan Rosen and Nick Smallbone. 2012. HipSpec: Automating Inductive Proofs of Program Properties. 16\u20135. https:\/\/doi.org\/10.29007\/3qwr 10.29007\/3qwr","DOI":"10.29007\/3qwr"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_23"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13977-2_3"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"e_1_3_1_20_2","unstructured":"Thierry Coquand and G\u00e9rard Huet. 1986. The Calculus of Constructions."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_22_2","unstructured":"Samuel G\u00e9lineau. 2010. Commutative Composition: a conservative approach to aspect weaving. https:\/\/escholarship.mcgill.ca\/concern\/theses\/gq67jr62t"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523731"},{"key":"e_1_3_1_25_2","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton","year":"2003","unstructured":"Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993562"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_3_1_28_2","volume-title":"MPI: The Complete Reference","author":"Snir M.","year":"1996","unstructured":"M. Snir, W. Otto, S. Huss-Lederman, D.W. Walker and J. Dongarra. 1996. MPI: The Complete Reference. MIT Press."},{"key":"e_1_3_1_29_2","doi-asserted-by":"crossref","unstructured":"Luca De Martini Alessandro Margara Gianpaolo Cugola Marco Donadoni and Edoardo Morassutto. 2023. The Noir Dataflow Platform: Efficient Data Processing without Complexity. arXiv:2306.04421 [cs.DC]","DOI":"10.1016\/j.future.2024.06.018"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10489-017-0954-8"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Derek G Murray Frank McSherry Rebecca Isaacs Michael Isard Paul Barham and Mart\u00edn Abadi. 2013. Naiad: a timely dataflow system. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. 439\u2013455.","DOI":"10.1145\/2517349.2522738"},{"key":"e_1_3_1_32_2","unstructured":"M. Saqib Nawaz Moin Malik Yi Li Meng Sun and M. Ikram Ullah Lali. 2019. A Survey on Theorem Provers in Formal Methods. arXiv:1912.03028 [cs.SE]"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/909447"},{"key":"e_1_3_1_34_2","unstructured":"The University of Glasgow. 2023. Prelude. https:\/\/hackage.haskell.org\/package\/base-4.19.0.0\/docs\/Prelude.html. Last accessed on 16 Nov 2023."},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/277830.277870"},{"key":"e_1_3_1_36_2","first-page":"254","volume-title":"Conceptual Modeling: Foundations and Applications - Essays in Honor of John Mylopoulos (Lecture Notes in Computer Science, Vol. 5600)","author":"Pottinger Rachel","year":"2009","unstructured":"Rachel Pottinger and Philip A. Bernstein. 2009. Associativity and Commutativity in Generic Merge. In Conceptual Modeling: Foundations and Applications - Essays in Honor of John Mylopoulos (Lecture Notes in Computer Science, Vol. 5600), Alexander Borgida, Vinay K. Chaudhri, Paolo Giorgini, and Eric S. K. Yu (Eds.). Springer, 254\u2013272."},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-012722442-8\/50081-1"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269969"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_6"},{"key":"e_1_3_1_44_2","unstructured":"Willam Sonnex Sophia Drossopoulou and Susan Eisenbach. 2011. Zeno: A tool for the automatic verification of algebraic properties of functional programs."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_28"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_27"},{"key":"e_1_3_1_47_2","article-title":"Conditional Lemma Discovery and Recursion Induction in Hipster","volume":"72","author":"Valbuena Irene Lobo","year":"2015","unstructured":"Irene Lobo Valbuena and Moa Johansson. 2015. Conditional Lemma Discovery and Recursion Induction in Hipster. Electronic Communications of the EASST 72 (2015).","journal-title":"Electronic Communications of the EASST"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.9728"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32254-2_12"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30048-7_35"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591276"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","unstructured":"George Zakhour Pascal Weisenburger and Guido Salvaneschi. 2024. Automated Verification of Fundamental Algebraic Laws. https:\/\/doi.org\/10.5281\/zenodo.10949342 10.5281\/zenodo.10949342","DOI":"10.5281\/zenodo.10949342"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656408","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:40:00Z","timestamp":1751661600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656408"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656408"],"URL":"https:\/\/doi.org\/10.1145\/3656408","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}