{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:17Z","timestamp":1750219817310,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"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,4,6]]},"abstract":"<jats:p>\n            The ubiquity of distributed agreement protocols, such as consensus, has galvanized interest in verification of such protocols\n            <jats:italic>as well as<\/jats:italic>\n            applications built on top of them. The complexity and unboundedness of such systems, however, makes their verification onerous in general, and, particularly prohibitive for full automation. An exciting, recent breakthrough reveals that, through careful modeling, it becomes possible to reduce verification of interesting distributed agreement-based (DAB) systems, that are unbounded in the number of processes, to model checking of small, finite-state systems. It is an open question if such reductions are also possible for DAB systems that are\n            <jats:italic>doubly-unbounded<\/jats:italic>\n            , in particular, DAB systems that additionally have unbounded data domains. We answer this question in the affirmative in this work thereby broadening the class of DAB systems which can be automatically and efficiently verified. We present a novel reduction which leverages\n            <jats:italic>value symmetry<\/jats:italic>\n            and a new notion of\n            <jats:italic>data saturation<\/jats:italic>\n            to reduce verification of doubly-unbounded DAB systems to model checking of small, finite-state systems. We develop a tool, Venus, that can efficiently verify sophisticated DAB system models such as the arbitration mechanism for a consortium blockchain, a distributed register, and a simple key-value store.\n          <\/jats:p>","DOI":"10.1145\/3586033","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"172-200","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8157-897X","authenticated-orcid":false,"given":"Christopher","family":"Wagner","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-7300-9382","authenticated-orcid":false,"given":"Nouraldin","family":"Jaber","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2456-217X","authenticated-orcid":false,"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0406-x"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_17"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_23"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-017-0302-6"},{"key":"e_1_2_1_6_1","unstructured":"Zachary Amsden Ramnik Arora Shehar Bano Mathieu Baudet Sam Blackshear Abhay Bothra George Cabrera andChristian Catalini Konstantinos Chalkias Evan Cheng Avery Ching Andrey Chursin George Danezis andGerardo Di Giacomo David L. Dill Hui Ding Nick Doudchenko Victor Gao Zhenhuan Gao Fran\u00e7ois Garillot Michael Gorven Philip Hayes J. Mark Hou Yuxuan Hu Kevin Hurley Kevin Lewi Chunqi Li Zekun Li Dahlia Malkhi andSonia Margulis Ben Maurer Payman Mohassel Ladi de Naurois Valeria Nikolaenko Todd Nowacki Oleksandr Orlov andDmitri Perelman Alistair Pott Brett Proctor Shaz Qadeer Rain Dario Russi Bryan Schwab Stephane Sezer Alberto Sonnino Herman Venter Lei Wei Nils Wernerfelt Brandon Williams Qinfan Wu Xifan Yan Tim Zakian and Runtian Zhou. 2020. The Libra Blockchain. https:\/\/developers.libra.org\/docs\/assets\/papers\/the-libra-blockchain\/2020-05-26.pdf \t\t\t\t  Zachary Amsden Ramnik Arora Shehar Bano Mathieu Baudet Sam Blackshear Abhay Bothra George Cabrera andChristian Catalini Konstantinos Chalkias Evan Cheng Avery Ching Andrey Chursin George Danezis andGerardo Di Giacomo David L. Dill Hui Ding Nick Doudchenko Victor Gao Zhenhuan Gao Fran\u00e7ois Garillot Michael Gorven Philip Hayes J. Mark Hou Yuxuan Hu Kevin Hurley Kevin Lewi Chunqi Li Zekun Li Dahlia Malkhi andSonia Margulis Ben Maurer Payman Mohassel Ladi de Naurois Valeria Nikolaenko Todd Nowacki Oleksandr Orlov andDmitri Perelman Alistair Pott Brett Proctor Shaz Qadeer Rain Dario Russi Bryan Schwab Stephane Sezer Alberto Sonnino Herman Venter Lei Wei Nils Wernerfelt Brandon Williams Qinfan Wu Xifan Yan Tim Zakian and Runtian Zhou. 2020. The Libra Blockchain. https:\/\/developers.libra.org\/docs\/assets\/papers\/the-libra-blockchain\/2020-05-26.pdf"},{"key":"e_1_2_1_7_1","unstructured":"Atomix. 2021. Atomix. https:\/\/atomix.io\/docs\/latest\/user-manual\/primitives\/AtomicValue\/ \t\t\t\t  Atomix. 2021. Atomix. https:\/\/atomix.io\/docs\/latest\/user-manual\/primitives\/AtomicValue\/"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_23"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951860.2951873"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 353\u2013362","author":"Clarke E.","year":"1861","unstructured":"E. Clarke , D. Long , and K. McMillan . 1989. Compositional Model Checking . In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 353\u2013362 . isbn:08 1861 9546 https:\/\/dl.acm.org\/doi\/abs\/10.5555\/77350.77387 E. Clarke, D. Long, and K. McMillan. 1989. Compositional Model Checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 353\u2013362. isbn:0818619546 https:\/\/dl.acm.org\/doi\/abs\/10.5555\/77350.77387"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028741"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_9"},{"volume-title":"Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS \u201900)","author":"Emerson E. Allen","key":"e_1_2_1_14_1","unstructured":"E. Allen Emerson , John W. Havlicek , and Richard J. Trefler . 2000. Virtual Symmetry Reduction . In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS \u201900) . IEEE Computer Society, USA. 121. isbn:0769507255 https:\/\/dl.acm.org\/doi\/abs\/10.5555\/788022.788994 E. Allen Emerson, John W. Havlicek, and Richard J. Trefler. 2000. Virtual Symmetry Reduction. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS \u201900). IEEE Computer Society, USA. 121. isbn:0769507255 https:\/\/dl.acm.org\/doi\/abs\/10.5555\/788022.788994"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_19"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/262004.262008"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782630"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409005"},{"key":"e_1_2_1_22_1","unstructured":"Hyperledger. 2021. The Hyperledger Project. https:\/\/www.hyperledger.org\/ \t\t\t\t  Hyperledger. 2021. The Hyperledger Project. https:\/\/www.hyperledger.org\/"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625968"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_15"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485534"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_12"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289237"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_34_1","unstructured":"Redis. 2021. Redis. https:\/\/redis.io\/ \t\t\t\t  Redis. 2021. Redis. https:\/\/redis.io\/"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90211-6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586033","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586033","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586033","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586033"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":40,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586033"],"URL":"https:\/\/doi.org\/10.1145\/3586033","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}