{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:17:08Z","timestamp":1784837828829,"version":"3.55.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["389792660 TRR 248--CPEC"],"award-info":[{"award-number":["389792660 TRR 248--CPEC"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["SCEPROOF"],"award-info":[{"award-number":["SCEPROOF"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    We present a technique for the verification of liveness properties of randomized distributed algorithms. Our technique gives SMT-based proofs for many common consensus algorithms, both for crash faults and for Byzantine faults. It is based on a sound proof rule for\n                    <jats:italic toggle=\"yes\">fair almost-sure termination<\/jats:italic>\n                    of distributed systems that combines martingale-based techniques for almost-sure termination with reasoning about weak fairness.\n                  <\/jats:p>\n                  <jats:p>Our proof rule is able to handle parametrized protocols where the state grows unboundedly and every variant function is unbounded. These protocols were out of scope for previous approaches, which either relied on bounded variant functions or on reductions to (non-probabilistic) fairness.<\/jats:p>\n                  <jats:p>We have implemented our proof rules on top of Caesar, a program verifier for probabilistic programs. We use our proof rule to give SMT-based proofs for termination properties of randomized asynchronous consensus protocols, including Ben-Or\u2019s protocol and graded binary consensus, for both crash and Byzantine faults. These protocols have notoriously difficult proofs of termination but fall within the scope of our proof rule.<\/jats:p>","DOI":"10.1145\/3776691","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1412-1441","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Almost-Sure Termination for Randomized Distributed Algorithms"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2727-8865","authenticated-orcid":false,"given":"Constantin","family":"Enea","sequence":"first","affiliation":[{"name":"LIX - Ecole Polytechnique - Institut Polytechnique de Paris, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2142-4254","authenticated-orcid":false,"given":"Harshit Jitendra","family":"Motwani","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5187-5415","authenticated-orcid":false,"given":"V. R.","family":"Sathiyanarayana","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:7)2007"},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"Ittai Abraham Naama Ben-David and Sravya Yandamuri. 2022. Efficient and adaptively secure asynchronous binary agreement via binding crusader agreement. In Proceedings of the 2022 ACM Symposium on Principles of Distributed Computing. 381\u2013391.","DOI":"10.1145\/3519270.3538426"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00446-012-0162-Z"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/983102"},{"key":"e_1_3_2_10_2","unstructured":"Kevin Stefan Batz. 2024. Automated deductive verification of probabilistic programs. Ph. D. Dissertation. RWTH Aachen University."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806707"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2016.101"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-020-00603-X"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_11"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:21)2022"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167105"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649824"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289519"},{"key":"e_1_3_2_21_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/6156.001.0001"},{"key":"e_1_3_2_23_2","first-page":"viii+654","volume-title":"Stochastic processes","author":"Doob J. L.","year":"1953","unstructured":"J. L. Doob. 1953. Stochastic processes. John Wiley & Sons, New York. viii+654 pages. MR 15,445b. Zbl 0053.26802.."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100026396"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_3_2_27_2","volume-title":"Fairness","author":"Francez Nissim","year":"2012","unstructured":"Nissim Francez. 2012. Fairness. Springer Science & Business Media."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSN58291.2024.00047"},{"key":"e_1_3_2_29_2","volume-title":"Probability and random processes","author":"Grimmett Geoffrey","year":"2020","unstructured":"Geoffrey Grimmett and David Stirzaker. 2020. Probability and random processes. Oxford university press."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80014-0"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90005-5"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2025.3567423"},{"key":"e_1_3_2_34_2","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation. RWTH Aachen University Germany. http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_2_36_2","unstructured":"Stephen Cole Kleene. 1952. Introduction to metamathematics. (1952)."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_13"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_17"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10843-2_22"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"Daniel Lehmann and Michael O Rabin. 1981. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 133\u2013138.","DOI":"10.1145\/567532.567547"},{"key":"e_1_3_2_43_2","volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","year":"1996","unstructured":"Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4002-0"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632879"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704899"},{"key":"e_1_3_2_47_2","unstructured":"Christoph Matheja. 2020. Automated reasoning and randomization in separation logic. Ph. D. Dissertation. RWTH Aachen University Germany. https:\/\/publications.rwth-aachen.de\/record\/780877"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/B138392"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01843570"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008917"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108680134"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1983.28"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622870"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_15"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:38:50Z","timestamp":1784209130000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776691"],"URL":"https:\/\/doi.org\/10.1145\/3776691","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}