{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T23:17:00Z","timestamp":1768346220328,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030255428","type":"print"},{"value":"9783030255435","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_20","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:09Z","timestamp":1562932989000},"page":"344-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Communication-Closed Asynchronous Protocols"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Damian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cezara","family":"Dr\u0103goi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru","family":"Militaru","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-73721-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2018","unstructured":"Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., Zuleger, F.: Parameterized model checking of synchronous distributed algorithms by abstraction. In: Dillig, I., Palsberg, J. (eds.) VMCAI 2018. LNCS, vol. 10747, pp. 1\u201324. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-73721-8_1"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Bakst, A., von Gleissenthall, K., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. PACMPL 1(OOPSLA), 110:1\u2013110:27 (2017)","DOI":"10.1145\/3133934"},{"key":"20_CR3","unstructured":"Bendersky, E.: pycparser. \n                      https:\/\/github.com\/eliben\/pycparser\n                      \n                    . Accessed 7 Nov 2018"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-319-96142-2_23","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2018","unstructured":"Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part II. LNCS, vol. 10982, pp. 372\u2013391. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96142-2_23"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Chandra, T.D., Griesemer, R., Redstone, J.: Paxos made live: an engineering perspective. In: PODC, pp. 398\u2013407 (2007)","DOI":"10.1145\/1281100.1281103"},{"issue":"2","key":"20_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225\u2013267 (1996)","journal-title":"J. ACM"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-04420-5_10","volume-title":"Reachability Problems","author":"M Chaouch-Saad","year":"2009","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 93\u2013106. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-04420-5_10"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-24550-3_11","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"B Charron-Bost","year":"2011","unstructured":"Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 120\u2013134. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-24550-3_11"},{"issue":"1","key":"20_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s00446-009-0084-6","volume":"22","author":"B Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distrib. Comput. 22(1), 49\u201371 (2009)","journal-title":"Distrib. Comput."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: PODC, pp. 44\u201365 (1988)","DOI":"10.1145\/62546.62556"},{"key":"20_CR11","unstructured":"Debrat, H., Merz, S.: Verifying fault-tolerant distributed algorithms in the heard-of model. In: Archive of Formal Proofs 2012 (2012)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almost-synchronous reductions. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, Part of SPLASH 2014, Portland, OR, USA, 20\u201324 October 2014, pp. 709\u2013725 (2014)","DOI":"10.1145\/2714064.2660211"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-54013-4_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Dr\u0103goi","year":"2014","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161\u2013181. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54013-4_10"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL, pp. 400\u2013415 (2016)","DOI":"10.1145\/2914770.2837650"},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. JACM 35(2), 288\u2013323 (1988)","journal-title":"JACM"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21\u201323 January 2009, pp. 2\u201315 (2009)","DOI":"10.1145\/1480881.1480885"},{"issue":"3","key":"20_CR17","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T Elrad","year":"1982","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155\u2013173 (1982)","journal-title":"Sci. Comput. Program."},{"key":"20_CR18","unstructured":"Gafni, E.: Round-by-round fault detectors: unifying synchrony and asynchrony (extended abstract). In: PODC, pp. 143\u2013152 (1998)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"912","DOI":"10.1007\/978-3-319-89884-1_32","volume-title":"Programming Languages and Systems","author":"\u00c1 Garc\u00eda-P\u00e9rez","year":"2018","unstructured":"Garc\u00eda-P\u00e9rez, \u00c1., Gotsman, A., Meshman, Y., Sergey, I.: Paxos consensus, deconstructed and abstracted. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 912\u2013939. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89884-1_32"},{"issue":"POPL","key":"20_CR20","first-page":"59:1","volume":"3","author":"K Gleissenthall von","year":"2019","unstructured":"von Gleissenthall, K., G\u00f6khan Kici, R., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3(POPL), 59:1\u201359:30 (2019)","journal-title":"PACMPL"},{"issue":"7","key":"20_CR21","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/3068608","volume":"60","author":"C Hawblitzel","year":"2017","unstructured":"Hawblitzel, C., et al.: IronFleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017)","journal-title":"Commun. ACM"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-17164-2_21","volume-title":"Programming Languages and Systems","author":"B Jacobs","year":"2010","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the verifast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304\u2013311. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-17164-2_21"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719\u2013734 (2017)","DOI":"10.1145\/3093333.3009860"},{"key":"20_CR24","unstructured":"Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR, pp. 21:1\u201321:17 (2018)"},{"key":"20_CR25","unstructured":"Lamport, L.: Generalized consensus and paxos. Technical report, March 2005. \n                      https:\/\/www.microsoft.com\/en-us\/research\/publication\/generalized-consensus-and-paxos\/"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: POPL, pp. 357\u2013370 (2016)","DOI":"10.1145\/2914770.2837622"},{"issue":"12","key":"20_CR27","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"20_CR28","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-63390-9_12","volume-title":"Computer Aided Verification","author":"O Mari\u0107","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017, Part II. LNCS, vol. 10427, pp. 217\u2013237. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12"},{"key":"20_CR30","unstructured":"Mattern, F.: On the relativistic structure of logical time in distributed systems. In: Parallel and Distributed Algorithms, pp. 215\u2013226 (1989)"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Moraru, I., Andersen, D.G., Kaminsky, M.: There is more consensus in Egalitarian parliaments. In: SOSP, pp. 358\u2013372 (2013)","DOI":"10.1145\/2517349.2517350"},{"issue":"4","key":"20_CR32","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1137\/S0097539799364006","volume":"31","author":"Y Moses","year":"2002","unstructured":"Moses, Y., Rajsbaum, S.: A layered analysis of consensus. SIAM J. Comput. 31(4), 989\u20131021 (2002)","journal-title":"SIAM J. Comput."},{"key":"20_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Oki, B.M., Liskov, B.: Viewstamped replication: a general primary copy. In: PODC, pp. 8\u201317 (1988)","DOI":"10.1145\/62546.62549"},{"key":"20_CR35","unstructured":"Ongaro, D., Ousterhout, J.K.: In search of an understandable consensus algorithm. In: 2014 USENIX Annual Technical Conference, USENIX ATC 2014, pp. 305\u2013319 (2014)"},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI, pp. 614\u2013630 (2016)","DOI":"10.1145\/2980983.2908118"},{"key":"20_CR37","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using EventML. ECEASST 72 (2015)"},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 28:1\u201328:30 (2018)","DOI":"10.1145\/3158116"},{"key":"20_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-17465-1_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"I Stoilkovska","year":"2019","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part II. LNCS, vol. 11428, pp. 357\u2013374. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-17465-1_20"},{"issue":"5\u20136","key":"20_CR40","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s00446-010-0123-3","volume":"23","author":"T Tsuchiya","year":"2011","unstructured":"Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrib. Comput. 23(5\u20136), 341\u2013358 (2011)","journal-title":"Distrib. Comput."},{"key":"20_CR41","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI, pp. 357\u2013368 (2015)","DOI":"10.1145\/2813885.2737958"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the RAFT consensus protocol. In: CPP, pp. 154\u2013165 (2016)","DOI":"10.1145\/2854065.2854081"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25543-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:08:52Z","timestamp":1562933332000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}