{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:08:15Z","timestamp":1776373695934,"version":"3.51.2"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"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":[[2023,1,9]]},"abstract":"<jats:p>The importance of exploiting<jats:italic>commutativity relations<\/jats:italic>in verification algorithms for concurrent programs is well-known. They can help simplify the proof and improve the time and space efficiency. This paper studies commutativity relations as a first-class object in the setting of verification algorithms for concurrent programs. A first contribution is a general framework for<jats:italic>abstract commutativity relations<\/jats:italic>. We introduce a general soundness condition for commutativity relations, and present a method to automatically derive sound abstract commutativity relations from a given proof. The method can be used in a verification algorithm based on abstraction refinement to compute a new commutativity relation in each iteration of the abstraction refinement loop. A second result is a general proof rule that allows one to combine multiple commutativity relations, with incomparable power, in a<jats:italic>stratified<\/jats:italic>way that preserves soundness and allows one to profit from the full power of the combined relations. We present an algorithm for the stratified proof rule that performs an optimal combination (in a sense made formal), enabling usage of stratified commutativity in algorithmic verification. We empirically evaluate the impact of abstract commutativity and stratified combination of commutativity relations on verification algorithms for concurrent programs.<\/jats:p>","DOI":"10.1145\/3571242","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1426-1453","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Stratified Commutativity in Verification Algorithms for Concurrent Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-2653","authenticated-orcid":false,"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[{"name":"University of Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2540-9489","authenticated-orcid":false,"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0469-y"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_17"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_14"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023. Appendix to: Stratified Commutativity in Verification Algorithms for Concurrent Programs. Uploaded as supplementary material to this paper in the ACM Digital Library Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2023. Appendix to: Stratified Commutativity in Verification Algorithms for Concurrent Programs. Uploaded as supplementary material to this paper in the ACM Digital Library","DOI":"10.1145\/3571242"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_5"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789814261456_0006"},{"key":"e_1_2_2_19_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\/ 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\/10.1145\/3571242","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571242","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571242"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":19,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571242"],"URL":"https:\/\/doi.org\/10.1145\/3571242","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}