{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:15Z","timestamp":1784830875302,"version":"3.55.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            <jats:italic toggle=\"yes\">Commutativity<\/jats:italic>\n            has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based\n            <jats:italic toggle=\"yes\">reduction<\/jats:italic>\n            of a program may admit simpler proofs than the program itself. The framework of lexicographical program reductions was introduced to formalize a broad class of reductions which accommodate sequential (thread-local) reasoning as well as synchronous programs. Approaches based on this framework, however, were fundamentally limited to program models with a\n            <jats:italic toggle=\"yes\">fixed\/bounded<\/jats:italic>\n            number of threads. In this paper, we show that it is possible to define an effective parametric family of program reductions that can be used to find simple proofs for\n            <jats:italic toggle=\"yes\">parameterized programs<\/jats:italic>\n            , i.e., for programs with an unbounded number of threads. We show that reductions are indeed useful for the simplification of proofs for parameterized programs, in a sense that can be made precise: A reduction of a parameterized program may admit a proof which uses\n            <jats:italic toggle=\"yes\">fewer<\/jats:italic>\n            or\n            <jats:italic toggle=\"yes\">less sophisticated<\/jats:italic>\n            ghost variables. The reduction may therefore be within reach of an automated verification technique, even when the original parameterized program is not. As our first technical contribution, we introduce a notion of reductions for parameterized programs such that the reduction\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">R<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            of a parameterized program\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">P<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is again a parameterized program (the thread template of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">R<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is obtained by source-to-source transformation of the thread template of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">P<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            ). Consequently, existing techniques for the verification of parameterized programs can be directly applied to\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">R<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            instead of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"script\">P<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . Our second technical contribution is that we define an appropriate family of\n            <jats:italic toggle=\"yes\">pairwise preference<\/jats:italic>\n            orders which can be effectively used as a parameter to produce different lexicographical reductions. To determine whether this theoretical foundation amounts to a usable solution in practice, we have implemented the approach, based on a recently proposed framework for parameterized program verification. The results of our preliminary experiments on a representative set of examples are encouraging.\n          <\/jats:p>","DOI":"10.1145\/3632925","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2485-2513","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Commutativity Simplifies Proofs of Parameterized Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2540-9489","authenticated-orcid":false,"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_19"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_14"},{"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.1145\/1480881.1480885"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806613"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan. 2013. Commutativity in Automated Verification. In LICS. 1\u201317. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175734 10.1109\/LICS56636.2023.10175734","DOI":"10.1109\/LICS56636.2023.10175734"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677012"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023a. Benchmarks for POPL'24 Paper \u201cCommutativity Simplifies Proofs of Parameterized Programs\u201d https:\/\/doi.org\/10.5281\/zenodo.10119773 10.5281\/zenodo.10119773","DOI":"10.5281\/zenodo.10119773"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023b. Commutativity Simplifies Proofs of Parameterized Programs (Extended Version). Technical Report https:\/\/dominik-klumpp.net\/publications\/popl24\/extended.pdf","DOI":"10.1145\/3632925"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428224"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2367430.2367439"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Hossein Hojjat Philipp R\u00fcmmer and Pavle Subotic. 2014. Horn Clauses for Communicating Timed Systems. In Proceedings First Workshop on Horn Clauses for Verification and Synthesis HCVS 2014 Vienna Austria 17 fuly 2014 (EPTCS Vol. 169) Nikolaj S. Bj\u00f8rner Fabio Fioravanti Andrey Rybalchenko and Valerio Valerio (Eds.). 39\u201352. https:\/\/doi.org\/10.4204\/EPTCS.169.6 10.4204\/EPTCS.169.6","DOI":"10.4204\/EPTCS.169.6"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_11"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_3_1_29_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie. 2 (June 2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-isboogie-2-2\/"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_18"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2001.925138"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987612"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679412"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632925","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632925","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:38Z","timestamp":1751659538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632925"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632925"],"URL":"https:\/\/doi.org\/10.1145\/3632925","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}