{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:57Z","timestamp":1750220697820,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,2,24]],"date-time":"2020-02-24T00:00:00Z","timestamp":1582502400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2020,2,24]]},"abstract":"<jats:p>Randomization is a powerful paradigm to solve hard problems, especially in distributed computing. Proving the correctness, and assessing the performances, of randomized distributed algorithms, is a very challenging research objective, that the verification community has started to address. In this article, we review existing model checking approaches to the verification of randomized distributed algorithms and identify further research directions.<\/jats:p>","DOI":"10.1145\/3385634.3385638","type":"journal-article","created":{"date-parts":[[2020,2,24]],"date-time":"2020-02-24T21:19:35Z","timestamp":1582579175000},"page":"35-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Model checking randomized distributed algorithms"],"prefix":"10.1145","volume":"7","author":[{"given":"Nathalie","family":"Bertrand","sequence":"first","affiliation":[{"name":"Univ. Rennes, Inria, CNRS, IRISA - Rennes (France)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,2,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0216-8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-012-0162-z"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/295656.295659"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1011767.1011810"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-005-0138-3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146381.1146425"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0196-6774(02)00220-1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89707-1\\_5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806707"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.33"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3\\_34"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209110"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.33"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.03.002"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.01.001"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.8"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2016.106"},{"key":"e_1_2_1_19_1","unstructured":"ByMC. ByMC: Byzantine Model Checker. http:\/\/www.forsyte.at\/software\/bymc\/. (????). Accessed Dec. 2019.  ByMC. ByMC: Byzantine Model Checker. http:\/\/www.forsyte.at\/software\/bymc\/. (????). Accessed Dec. 2019."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-005-0318-0"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2011.36"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45489-3_4"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-003-0102-z"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2014.1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-58747-9\\_2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.470"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2016.27"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0272-3"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03424-5\\_22"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/135419.135468"},{"key":"e_1_2_1_39_1","volume-title":"Kwiatkowska and Gethin Norman","author":"Marta","year":"2002","unstructured":"Marta Z. Kwiatkowska and Gethin Norman . 2002 . Verifying Randomized Byzantine Agreement. In FORTE. 194--209. Marta Z. Kwiatkowska and Gethin Norman. 2002. Verifying Randomized Byzantine Agreement. In FORTE. 194--209."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0227-6"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_17"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_11"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 21st International Conference on Principles of Distributed Systems (OPODIS'17)","author":"Lazic Marijana","year":"2017","unstructured":"Marijana Lazic , Igor Konnov , Josef Widder , and Roderick Bloem . 2017 . Synthesis of Distributed Algorithms with Parameterized Threshold Guards . In Proceedings of the 21st International Conference on Principles of Distributed Systems (OPODIS'17) . (to appear). Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem. 2017. Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In Proceedings of the 21st International Conference on Principles of Distributed Systems (OPODIS'17). (to appear)."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567547"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5\\_29"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6\\_7"},{"key":"e_1_2_1_47_1","unstructured":"Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann.  Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2008.8"},{"key":"e_1_2_1_49_1","unstructured":"Prism. PRISM case studies. http:\/\/www.prismmodelchecker.org\/casestudies\/index.php. (????). Accessed Dec. 2019.  Prism. PRISM case studies. http:\/\/www.prismmodelchecker.org\/casestudies\/index.php. (????). Accessed Dec. 2019."},{"volume-title":"Algorithms and Complexity: New directions and recent results","author":"Rabin Michael O.","key":"e_1_2_1_50_1","unstructured":"Michael O. Rabin . 1976. Probabilistic Algorithms . In Algorithms and Complexity: New directions and recent results . Academic Press , 21--39. Michael O. Rabin. 1976. Probabilistic Algorithms. In Algorithms and Complexity: New directions and recent results. Academic Press, 21--39."},{"key":"e_1_2_1_52_1","unstructured":"Storm. STORM model checker. http:\/\/www.stormchecker.org\/index.html. (????). Accessed Dec. 2019.  Storm. STORM model checker. http:\/\/www.stormchecker.org\/index.html. (????). Accessed Dec. 2019."}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385634.3385638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385634.3385638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:49Z","timestamp":1750199569000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385634.3385638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,24]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2,24]]}},"alternative-id":["10.1145\/3385634.3385638"],"URL":"https:\/\/doi.org\/10.1145\/3385634.3385638","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2020,2,24]]},"assertion":[{"value":"2020-02-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}