{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T22:22:39Z","timestamp":1770243759458,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"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,10,8]]},"abstract":"<jats:p>We describe the design and implementation of Must, a framework for modeling and automatically verifying distributed systems. Must provides a concurrency API that supports multiple communication models, on top of a mainstream programming language, such as Rust. Given a program using this API, Must verifies it by means of a novel, optimal dynamic partial order reduction algorithm that maintains completeness and optimality for all communication models supported by the API.<\/jats:p>\n                  <jats:p>We use Must to design and verify models of distributed systems in an industrial context. We demonstrate the usability of Must\u2019s API by modeling high-level system idioms (e.g., timeouts, leader election, versioning) as abstractions over the core API, and demonstrate Must\u2019s scalability by verifying systems employed in production (e.g., replicated logs, distributed transaction management protocols), the verification of which lies beyond the capacity of previous model checkers.<\/jats:p>","DOI":"10.1145\/3689778","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1900-1927","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Model Checking Distributed Protocols in Must"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"first","affiliation":[{"name":"AWS, Paris, France"},{"name":"Ecole Polytechnique, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1158-526X","authenticated-orcid":false,"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[{"name":"AWS, Santa Clara, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"},{"name":"AWS, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"353","volume-title":"TACAS 2015 (LNCS)","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. \u201cStateless model checking for TSO and PSO.\u201d In: TACAS 2015 (LNCS). Vol. 9035. Springer, Berlin, Heidelberg, 353\u2013367. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28 10.1007\/978-3-662-46681-0_28."},{"key":"e_1_3_1_3_1","first-page":"373","volume-title":"POPL 2014","author":"Abdulla Parosh Aziz","year":"2014","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. \u201cOptimal dynamic partial order reduction.\u201d In: POPL 2014. ACM, New York, NY, USA, 373\u2013384. https:\/\/doi.org\/10.1145\/2535838.2535845 10.1145\/2535838.2535845."},{"key":"e_1_3_1_4_1","first-page":"150:1","article-title":"Optimal stateless model checking for reads-from equivalence under sequential consistency","volume":"3","author":"Abdulla Parosh Aziz","year":"2019","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lang, Tuan Phong Ngo, and Konstantinos Sagonas. Oct. 10, 2019. \u201cOptimal stateless model checking for reads-from equivalence under sequential consistency.\u201d Proc. ACM Program. Lang., 3, (Oct. 10, 2019), 150:1\u2013150:29, OOPSLA, (Oct. 10, 2019). https:\/\/doi.org\/10.1145\/3360576 10.1145\/3360576.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_5_1","first-page":"134","volume-title":"CAV 2016 (LNCS)","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. \u201cStateless model checking for POWER.\u201d In: CAV 2016 (LNCS). Vol. 9780. Springer, Berlin, Heidelberg, 134\u2013156. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8 10.1007\/978-3-319-41540-6_8."},{"key":"e_1_3_1_6_1","first-page":"135:1","article-title":"Optimal stateless model checking under the release-acquire semantics","volume":"2","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. Oct. 2018. \u201cOptimal stateless model checking under the release-acquire semantics.\u201d Proc. ACM Program. Lang., 2, OOPSLA, (Oct. 2018), 135:1\u2013135:29. https:\/\/doi.org\/10.1145\/3276505 10.1145\/3276505.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_7_1","first-page":"105","volume-title":"TACAS 2023 (LNCS)","author":"Abdulla Parosh Aziz","year":"2023","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, S. Krishna, Ashutosh Gupta, and Omkar Tuppe. 2023. \u201cOptimal Stateless Model Checking for Causal Consistency.\u201d In: TACAS 2023 (LNCS). Ed. by Sriram Sankaranarayanan and Natasha Sharygina. Vol. 13993. Springer, 105\u2013125. https:\/\/doi.org\/10.1007\/978-3-031-30823-9_6 10.1007\/978-3-031-30823-9_6."},{"key":"e_1_3_1_8_1","first-page":"341","volume-title":"CAV 2021","author":"Agarwal Pratyush","year":"2021","unstructured":"Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. July 2021. \u201cStateless Model Checking Under a Reads-Value-From Equivalence.\u201d In: CAV 2021. Ed. by Alexandra Silva and K. Rustan M. Leino. Springer International Publishing, Cham, (July 2021), 341\u2013366. isbn: 978-3-030-81685-8. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16 10.1007\/978-3-030-81685-8_16."},{"key":"e_1_3_1_9_1","first-page":"526","volume-title":"CAV 2017","author":"Albert Elvira","year":"2017","unstructured":"Elvira Albert, Puri Arenas, Mar\u00eda Garc\u00eda de la Banda, Miguel Gomez-Zamalloa, and Peter J. Stuckey. 2017. \u201cContext-sensitive dynamic partial order reduction.\u201d In: CAV 2017. Ed. by Rupak Majumdar and Viktor Kuncak. Springer International Publishing, Cham, 526\u2013543. isbn: 978-3-319-63387-9. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_26 10.1007\/978-3-319-63387-9_26."},{"key":"e_1_3_1_10_1","first-page":"392","volume-title":"CAV 2018","author":"Albert Elvira","year":"2018","unstructured":"Elvira Albert, Miguel Gomez-Zamalloa, Miguel Isabel, and Albert Rubio. 2018. \u201cConstrained dynamic partial order reduction.\u201d In: CAV 2018. Ed. by Hana Chockler and Georg Weissenbacher. Springer International Publishing, Cham, 392\u2013410. isbn: 978-3-319-96142-2. https:\/\/doi.org\/10.1007\/978-3-319-96142-2_24 10.1007\/978-3-319-96142-2_24."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_12_1","volume-title":"Data-centric Programming for Distributed Systems","author":"Alvaro Peter","year":"2015","unstructured":"Peter Alvaro. 2015. \u201cData-centric Programming for Distributed Systems.\u201d Ph.D. Dissertation. University of California, Santa Cruz, USA. http:\/\/www.escholarship.org\/uc\/item\/2296w4q3."},{"key":"e_1_3_1_13_1","first-page":"229","volume-title":"TACAS 2018 (LNCS)","author":"Aronis Stavros","year":"2018","unstructured":"Stavros Aronis, Bengt Jonsson, Magnus L\u00e4ng, and Konstantinos Sagonas. 2018. \u201cOptimal dynamic partial order reduction with observers.\u201d In: TACAS 2018 (LNCS). Vol. 10806. Springer, 229\u2013248. https:\/\/doi.org\/10.1007\/978-3-319-89963-3_14 10.1007\/978-3-319-89963-3_14."},{"key":"e_1_3_1_14_1","article-title":"Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels","volume":"7","author":"Bouajjani Ahmed","year":"2023","unstructured":"Ahmed Bouajjani, Constantin Enea, and Enrique Rom\u00e1n-Calvo. June 2023. \u201cDynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels.\u201d Proc. ACM Program. Lang., 7, PLDI, (June 2023). https:\/\/doi.org\/10.1145\/3591243 10.1145\/3591243.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_15_1","first-page":"31:1","article-title":"Data-centric dynamic partial order reduction","volume":"2","author":"Chalupa Marek","year":"2017","unstructured":"Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Dec. 2017. \u201cData-centric dynamic partial order reduction.\u201d Proc. ACM Program. Lang., 2, POPL, (Dec. 2017), 31:1\u201331:30. https:\/\/doi.org\/10.1145\/3158119 10.1145\/3158119.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_16_1","article-title":"Value-Centric Dynamic Partial Order Reduction","volume":"3","author":"Chatterjee Krishnendu","year":"2019","unstructured":"Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. Oct. 2019. \u201cValue-Centric Dynamic Partial Order Reduction.\u201d Proc. ACM Program. Lang., 3, OOPSLA, (Oct. 2019). https:\/\/doi.org\/10.1145\/3360550 10.1145\/3360550.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_17_1","first-page":"154","volume-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015","author":"Deligiannis Pantazis","year":"2015","unstructured":"Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson. 2015. \u201cAsynchronous programming, analysis and testing with state machines.\u201d In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. Ed. by David Grove and Stephen M. Blackburn. ACM, 154\u2013164. https:\/\/doi.org\/10.1145\/2737924.2737996 10.1145\/2737924.2737996."},{"key":"e_1_3_1_18_1","first-page":"108","volume-title":"SoCC \u201821: ACM Symposium on Cloud Computing, Seattle, WA, USA, November 1 - 4, 2021","author":"Deligiannis Pantazis","year":"2021","unstructured":"Pantazis Deligiannis, Narayanan Ganapathy, Akash Lal, and Shaz Qadeer. 2021. \u201cBuilding Reliable Cloud Services Using Coyote Actors.\u201d In: SoCC \u201821: ACM Symposium on Cloud Computing, Seattle, WA, USA, November 1 - 4, 2021. Ed. by Carlo Curino, Georgia Koutrika, and Ravi Netravali. ACM, 108\u2013121. https:\/\/doi.org\/10.1145\/3472883.3486983 10.1145\/3472883.3486983."},{"key":"e_1_3_1_19_1","first-page":"433","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II (Lecture Notes in Computer Science)","author":"Deligiannis Pantazis","year":"2023","unstructured":"Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett, and Akash Lal. 2023. \u201cIndustrial-Strength Controlled Concurrency Testing for sc C tt # Programs with sc Coyote.\u201d In: Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II (Lecture Notes in Computer Science). Ed. by Sriram Sankaranarayanan and Natasha Sharygina. Vol. 13994. Springer, 433\u2013452. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_26 10.1007\/978-3-031-30820-8_26."},{"key":"e_1_3_1_20_1","first-page":"321","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201813, Seattle, WA, USA, June 16-19, 2013","author":"Desai Ankush","year":"2013","unstructured":"Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram K. Rajamani, and Damien Zufferey. 2013. \u201cP: safe asynchronous event-driven programming.\u201d In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201813, Seattle, WA, USA, June 16-19, 2013. Ed. by Hans-Juergen Boehm and Cormac Flanagan. ACM, 321\u2013332. https:\/\/doi.org\/10.1145\/2491956.2462184 10.1145\/2491956.2462184."},{"key":"e_1_3_1_21_1","first-page":"159:1","article-title":"Compositional programming and testing of dynamic distributed systems","volume":"2","author":"Desai Ankush","year":"2018","unstructured":"Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. 2018. \u201cCompositional programming and testing of dynamic distributed systems.\u201d Proc. ACM Program. Lang., 2, OOPSLA, 159:1\u2013159:30. https:\/\/doi.org\/10.1145\/3276529 10.1145\/3276529.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_22_1","article-title":"A Partial Order View of Message-Passing Communication Models","volume":"7","author":"Di Giusto Cinzia","year":"2023","unstructured":"Cinzia Di Giusto, Davide Ferr\u00e9, Laetitia Laversa, and Etienne Lozes. 2023. \u201cA Partial Order View of Message-Passing Communication Models.\u201d Proc. ACM Program. Lang., 7, POPL. https:\/\/doi.org\/10.1145\/3571248 10.1145\/3571248.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_23_1","unstructured":"Erlang. 2023. Concurrent Programming. (). Retrieved July 12 2023 from https:\/\/www.erlang.org\/doc\/getting_started\/conc_prog.html."},{"key":"e_1_3_1_24_1","first-page":"110","volume-title":"POPL 2005","author":"Flanagan Cormac","year":"2005","unstructured":"Cormac Flanagan and Patrice Godefroid. 2005. \u201cDynamic partial-order reduction for model checking software.\u201d In: POPL 2005. ACM, New York, NY, USA, 110\u2013121. https:\/\/doi.org\/10.1145\/1040305.1040315 10.1145\/1040305.1040315."},{"key":"e_1_3_1_25_1","first-page":"174","article-title":"Model checking for programming languages using VeriSoft","author":"Godefroid Patrice","year":"1997","unstructured":"Patrice Godefroid. 1997. \u201cModel checking for programming languages using VeriSoft.\u201d In: POPL 1997. ACM, Paris, France, 174\u2013186. https:\/\/doi.org\/10.1145\/263699.263717 10.1145\/263699.263717.","journal-title":"POPL 1997"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_3_1_27_1","first-page":"51","volume-title":"Erlang 2011","author":"Gotovos Alkis","year":"2011","unstructured":"Alkis Gotovos, Maria Christakis, and Konstantinos Sagonas. 2011. \u201cTest-Driven Development of Concurrent Programs Using Concuerror.\u201d In: Erlang 2011. ACM, Tokyo, Japan, 51\u201361. isbn: 9781450308595. https:\/\/doi.org\/10.1145\/2034654.2034664 10.1145\/2034654.2034664."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3485534","article-title":"QuickSilver: modeling and parameterized verification for distributed agreement-based systems","volume":"5","author":"Jaber Nouraldin","year":"2021","unstructured":"Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, and Roopsha Samanta. 2021. \u201cQuickSilver: modeling and parameterized verification for distributed agreement-based systems.\u201d Proc. ACM Program. Lang., 5, OOPSLA, 1\u201331. https:\/\/doi.org\/10.1145\/3485534 10.1145\/3485534.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_30_1","volume-title":"NSDI 2007","author":"Killian Charles","year":"2007","unstructured":"Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. Apr. 2007. \u201cLife, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code.\u201d In: NSDI 2007. USENIX Association, Cambridge, MA, (Apr. 2007). https:\/\/www.usenix.org\/conference\/nsdi-07\/life-death-and-critical-transition-finding-liveness-bugs-systems-code."},{"key":"e_1_3_1_31_1","first-page":"179","volume-title":"PLDI 2007","author":"Killian Charles Edwin","year":"2007","unstructured":"Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin M. Vahdat. 2007. \u201cMace: Language Support for Building Distributed Systems.\u201d In: PLDI 2007. ACM, San Diego, California, USA, 179\u2013188. isbn: 9781595936332. https:\/\/doi.org\/10.1145\/1250734.1250755 10.1145\/1250734.1250755."},{"key":"e_1_3_1_32_1","article-title":"Truly stateless, optimal dynamic partial order reduction","volume":"6","author":"Kokologiannakis Michalis","year":"2022","unstructured":"Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. Jan. 2022. \u201cTruly stateless, optimal dynamic partial order reduction.\u201d Proc. ACM Program. Lang., 6, POPL, (Jan. 2022). https:\/\/doi.org\/10.1145\/3498711 10.1145\/3498711.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_33_1","doi-asserted-by":"crossref","unstructured":"Michalis Kokologiannakis Iason Marmanis and Viktor Vafeiadis. 2023. \u201cUnblocking Dynamic Partial Order Reduction.\u201d In: CAV 2023.","DOI":"10.1007\/978-3-031-37706-8_12"},{"key":"e_1_3_1_34_1","volume-title":"PLDI 2019","author":"Kokologiannakis Michalis","year":"2019","unstructured":"Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. \u201cModel checking for weakly consistent libraries.\u201d In: PLDI 2019. ACM, New York, NY, USA. https:\/\/doi.org\/10.1145\/3314221.3314609 10.1145\/3314221.3314609."},{"key":"e_1_3_1_35_1","first-page":"1157","volume-title":"ASPLOS 2020 (ASPLOS \u201820)","author":"Kokologiannakis Michalis","year":"2020","unstructured":"Michalis Kokologiannakis and Viktor Vafeiadis. 2020. \u201cHMC: Model checking for hardware memory models.\u201d In: ASPLOS 2020 (ASPLOS \u201820). ACM, Lausanne, Switzerland, 1157\u20131171. isbn: 9781450371025. https:\/\/doi.org\/10.1145\/3373376.3378480 10.1145\/3373376.3378480."},{"key":"e_1_3_1_36_1","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. isbn: 0-3211-4306-X. http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html."},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","unstructured":"Steven Lauterburg Mirco Dotta Darko Marinov and Gul Agha. 2009. \u201cA Framework for State-Space Exploration of Java-Based Actor Programs.\u201d In: ASE 2009 468\u2013479. https:\/\/doi.org\/10.1109\/ASE.2009.88 10.1109\/ASE.2009.88.","DOI":"10.1109\/ASE.2009.88"},{"key":"e_1_3_1_38_1","unstructured":"Loom. (). Retrieved July 6 2023 from https:\/\/github.com\/tokio-rs\/loom."},{"key":"e_1_3_1_39_1","first-page":"680","article-title":"Partial Order Reduction for Event-Driven Multithreaded Programs","author":"Maiya Pallavi","year":"2016","unstructured":"Pallavi Maiya, Rahul Gupta, Aditya Kanade, and Rupak Majumdar. 2016. \u201cPartial Order Reduction for Event-Driven Multithreaded Programs.\u201d In: TACAS 2016. Springer Berlin Heidelberg, Berlin, Heidelberg, 680\u2013697. isbn: 978-3-662-49674-9. https:\/\/doi.org\/10.1007\/978-3-662-49674-9_44 10.1007\/978-3-662-49674-9_44.","journal-title":"TACAS 2016"},{"key":"e_1_3_1_40_1","article-title":"Distributed System Fuzzing","author":"Meng Ruijie","year":"2023","unstructured":"Ruijie Meng, George Pirlea, Abhik Roychoudhury, and Ilya Sergey. 2023. \u201cDistributed System Fuzzing.\u201d CoRR, abs\/2305.02601. arXiv: 2305.02601. https:\/\/arxiv.org\/abs\/2305.02601 https:\/\/doi.org\/10.48550\/ARXIV.2305.02601 10.48550\/ARXIV.2305.02601.","journal-title":"CoRR"},{"key":"e_1_3_1_41_1","first-page":"267","article-title":"Finding and Reproducing Heisenbugs in Concurrent Programs","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, G\u00e9rard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. \u201cFinding and Reproducing Heisenbugs in Concurrent Programs.\u201d In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. Ed. by Richard Draves and Robbert van Renesse. USENIX Association, 267\u2013280. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full%5C_papers\/musuvathi\/musuvathi.pdf.","journal-title":"8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings"},{"key":"e_1_3_1_42_1","first-page":"131","article-title":"CDSChecker: Checking concurrent data structures written with C\/C++ atomics","author":"Norris Brian","year":"2013","unstructured":"Brian Norris and Brian Demsky. 2013. \u201cCDSChecker: Checking concurrent data structures written with C\/C++ atomics.\u201d In: OOPSLA 2013. ACM, 131\u2013150. https:\/\/doi.org\/10.1145\/2509136.2509514 10.1145\/2509136.2509514.","journal-title":"OOPSLA 2013"},{"key":"e_1_3_1_43_1","first-page":"160:1","article-title":"Randomized testing of distributed systems with probabilistic guarantees","volume":"2","author":"Ozkan Burcu Kulahcioglu","year":"2018","unstructured":"Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, and Georg Weissenbacher. 2018. \u201cRandomized testing of distributed systems with probabilistic guarantees.\u201d Proc. ACM Program. Lang., 2, OOPSLA, 160:1\u2013160:28. https:\/\/doi.org\/10.1145\/3276530 10.1145\/3276530.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_44_1","first-page":"614","volume-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016","author":"Padon Oded","year":"2016","unstructured":"Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. \u201cIvy: safety verification by interactive generalization.\u201d In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. Ed. by Chandra Krintz and Emery D. Berger. ACM, 614\u2013630. https:\/\/doi.org\/10.1145\/2908080.2908118 10.1145\/2908080.2908118."},{"key":"e_1_3_1_45_1","first-page":"91","article-title":"Chain Replication for Supporting High Throughput and Availability","author":"Renesse Robbert","year":"2004","unstructured":"Robbert van Renesse and Fred B. Schneider. 2004. \u201cChain Replication for Supporting High Throughput and Availability.\u201d In: 6th Symposium on Operating System Design and Implementation (OSDI 2004), San Francisco, California, USA, December 6-8, 2004. Ed. by Eric A. Brewer and Peter Chen. USENIX Association, 91\u2013104. http:\/\/www.usenix.org\/events\/osdi04\/tech\/renesse.html.","journal-title":"6th Symposium on Operating System Design and Implementation (OSDI 2004), San Francisco, California, USA, December 6-8, 2004"},{"key":"e_1_3_1_46_1","first-page":"456","volume-title":"CONCUR 2015 (LIPIcs)","author":"Rodr\u00edguez C\u00e9sar","year":"2015","unstructured":"C\u00e9sar Rodr\u00edguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. \u201cUnfolding-based Partial Order Reduction.\u201d In: CONCUR 2015 (LIPIcs). Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 456\u2013469. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.456 10.4230\/LIPIcs.CONCUR.2015.456."},{"key":"e_1_3_1_47_1","first-page":"339","volume-title":"FASE 2006","author":"Sen Koushik","year":"2006","unstructured":"Koushik Sen and Gul Agha. 2006. \u201cAutomated Systematic Testing of Open Distributed Programs.\u201d In: FASE 2006. Ed. by Luciano Baresi and Reiko Heckel. Springer Berlin Heidelberg, Berlin, Heidelberg, 339\u2013356. isbn: 978-3-540-33094-3. https:\/\/doi.org\/10.1007\/11693017_25 10.1007\/11693017_25."},{"key":"e_1_3_1_48_1","first-page":"28:1","article-title":"Programming and proving with distributed protocols","volume":"2","author":"Sergey Ilya","year":"2018","unstructured":"Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. \u201cProgramming and proving with distributed protocols.\u201d Proc. ACM Program. Lang., 2, POPL, 28:1\u201328:30. https:\/\/doi.org\/10.1145\/3158116 10.1145\/3158116.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_49_1","unstructured":"Shuttle. (). Retrieved July 6 2023 from https:\/\/github.com\/awslabs\/shuttle."},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.808407"},{"key":"e_1_3_1_51_1","first-page":"219","volume-title":"FORTE 2012","author":"Tasharofi Samira","year":"2012","unstructured":"Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. 2012. \u201cTransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs.\u201d In: FORTE 2012. Ed. by Holger Giese and Grigore Rosu. Springer Berlin Heidelberg, Berlin, Heidelberg, 219\u2013234. https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14 10.1007\/978-3-642-30793-5_14."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586053"},{"key":"e_1_3_1_53_1","article-title":"Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions","volume":"8","author":"Yao Jianan","year":"2024","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. Jan. 2024. \u201cMostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions.\u201d Proc. ACM Program. Lang., 8, POPL, (Jan. 2024). https:\/\/doi.org\/10.1145\/3632877 10.1145\/3632877.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_54_1","first-page":"366","volume-title":"Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018","author":"Yi Qiuping","year":"2018","unstructured":"Qiuping Yi and Jeff Huang. 2018. \u201cConcurrency verification with maximal path causality.\u201d In: Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018. Ed. by Gary T. Leavens, Alessandro Garcia, and Corina S. Pasareanu. ACM, 366\u2013376. https:\/\/doi.org\/10.1145\/3236024.3236048 10.1145\/3236024.3236048."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689778","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689778","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:06:17Z","timestamp":1770195977000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689778"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689778"],"URL":"https:\/\/doi.org\/10.1145\/3689778","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}