乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:54Z","timestamp":1740179334303,"version":"3.37.3"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,5]]},"abstract":"\n 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 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 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 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 fewer<\/jats:italic>\n or\n less sophisticated ghost variables<\/jats:italic>\n . 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 R<\/jats:italic>\n of a parameterized program\n P<\/jats:italic>\n is again a parameterized program (the thread template of\n R<\/jats:italic>\n is obtained by source-to-source transformation of the thread template of\n P<\/jats:italic>\n ). Consequently, existing techniques for the verification of parameterized programs can be directly applied to\n R<\/jats:italic>\n instead of\n P<\/jats:italic>\n . Our second technical contribution is that we define an appropriate family of\n pairwise preference orders<\/jats:italic>\n 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":4,"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"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1145\/2535838.2535845"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/3-540-44585-4_19"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/s10009-017-0469-y"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/978-3-319-13338-6_14"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/BFb0028741"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/1480881.1480885"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/1806596.1806613"},{"doi-asserted-by":"publisher","unstructured":"Azadeh Farzan. 2023. Commutativity in Automated Verification. In LICS. 1\u20137. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175734 10.1109\/LICS56636.2023.10175734","key":"e_1_2_1_8_1","DOI":"10.1109\/LICS56636.2023.10175734"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/2535838.2535885"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/2676726.2677012"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/3519939.3523727"},{"doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023. Benchmarks for POPL\u201924 Paper \"Commutativity Simplifies Proofs of Parameterized Programs\". https:\/\/doi.org\/10.5281\/zenodo.10119773 10.5281\/zenodo.10119773","key":"e_1_2_1_12_1","DOI":"10.5281\/zenodo.10119773"},{"doi-asserted-by":"crossref","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023. Commutativity Simplifies Proofs of Parameterized Programs (Extended Version). https:\/\/dominik-klumpp.net\/publications\/popl24\/extended.pdf","key":"e_1_2_1_13_1","DOI":"10.1145\/3632925"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-030-25540-4_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/3371081"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1145\/3428224"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_18_1","first-page":"1","article-title":"On Communicating Automata with Bounded Channels","volume":"80","author":"Genest Blaise","year":"2007","unstructured":"Blaise Genest, Dietrich Kuske, and Anca Muscholl. 2007. On Communicating Automata with Bounded Channels. Fundam. Inform., 80, 1-3 (2007), 147\u2013167.","journal-title":"Fundam. Inform."},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1007\/3-540-60761-7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/2254064.2254112"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/2950290.2950330"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/3009837.3009893"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.4204\/EPTCS.169.6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/978-3-642-02658-4_31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1007\/978-3-662-44584-6_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/3385412.3385980"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1007\/978-3-319-96145-3_5"},{"unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. June https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/","key":"e_1_2_1_28_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/361227.361234"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1007\/978-3-662-53413-7_18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1109\/IPDPS.2001.925138"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1007\/3-540-45319-9_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1109\/FMCAD.2014.6987612"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/3290372"},{"key":"e_1_2_1_35_1","volume-title":"FMCAD 2013","author":"Wachter Bj\u00f6rn","year":"2013","unstructured":"Bj\u00f6rn Wachter, Daniel Kroening, and Jo\u00ebl Ouaknine. 2013. Verifying multi-threaded software with Impact. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, 210\u2013217. http:\/\/ieeexplore.ieee.org\/document\/6679412\/"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632925","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T15:13:13Z","timestamp":1706541193000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632925"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,5]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,5]]}},"alternative-id":["10.1145\/3632925"],"URL":"https:\/\/doi.org\/10.1145\/3632925","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,1,5]]},"assertion":[{"value":"2024-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}