{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:50Z","timestamp":1781076050826,"version":"3.54.1"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030500856","type":"print"},{"value":"9783030500863","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-50086-3_11","type":"book-chapter","created":{"date-parts":[[2020,6,9]],"date-time":"2020-06-09T12:03:09Z","timestamp":1591704189000},"page":"189-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Tutorial: Parameterized Verification with Byzantine Model Checker"],"prefix":"10.1007","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijana","family":"Lazi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilina","family":"Stoilkovska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,8]]},"reference":[{"key":"11_CR1","unstructured":"Bounded Model Checking of STA. https:\/\/github.com\/istoilkovska\/syncTA"},{"key":"11_CR2","unstructured":"Abraham, I., Malkhi, D., Nayak, K., Ren, L., Spiegelman, A.: Solidus: an incentive-compatible cryptocurrency based on permissionless Byzantine consensus. CoRR abs\/1612.02916 (2016). http:\/\/arxiv.org\/abs\/1612.02916"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Aguilera, M., Toueg, S.: The correctness proof of Ben-Or\u2019s randomized consensus algorithm. Distributed Computing pp. 1\u201311 (2012)","DOI":"10.1007\/s00446-012-0162-z"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K Apt","year":"1986","unstructured":"Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. IPL 15, 307\u2013309 (1986)","journal-title":"IPL"},{"key":"11_CR5","first-page":"110:1","volume":"1(OOPSLA)","author":"A Bakst","year":"2017","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)","journal-title":"PACMPL"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., et al.: CVC4. In: CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract), In: PODC, pp. 27\u201330 (1983)","DOI":"10.1145\/800221.806707"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-030-25543-5_15","volume-title":"Computer Aided Verification","author":"I Berkovits","year":"2019","unstructured":"Berkovits, I., Lazi\u0107, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 245\u2013266. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Asymptotically optimal distributed consensus. Technical report, Bell Labs (1989). http:\/\/plan9.bell-labs.co\/who\/garay\/asopt.ps","DOI":"10.1109\/SFCS.1989.63511"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Towards optimal distributed consensus (Extended Abstract). In: FOCS, pp. 410\u2013415 (1989)","DOI":"10.1109\/SFCS.1989.63511"},{"key":"11_CR11","unstructured":"Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: CONCUR 2019, LIPIcs, vol. 140, pp. 33:1\u201333:15 (2019)"},{"key":"11_CR12","unstructured":"Bertrand, N., Konnov, I., Lazi\u0107, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: CONCUR, pp. 33:1\u201333:15 (2019)"},{"issue":"40","key":"11_CR13","doi-asserted-by":"publisher","first-page":"5602","DOI":"10.1016\/j.tcs.2010.09.032","volume":"412","author":"M Biely","year":"2011","unstructured":"Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theor. Comput. Sci. 412(40), 5602\u20135630 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR14","first-page":"193","volume":"1579","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. TACAS. LNCS 1579, 193\u2013207 (1999)","journal-title":"LNCS"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al..: Decidability of Parameterized Verification. Morgan & Claypool, Synthesis Lectures on Distributed Computing Theory (2015)","DOI":"10.1007\/978-3-031-02011-7"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: CAV. pp. 372\u2013391 (2018)","DOI":"10.1007\/978-3-319-96142-2_23"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1016\/0890-5401(87)90054-X","volume":"75","author":"G Bracha","year":"1987","unstructured":"Bracha, G.: Asynchronous Byzantine agreement protocols. Inf. Comput. 75(2), 130\u2013143 (1987)","journal-title":"Inf. Comput."},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"key":"11_CR19","first-page":"42","volume":"2127","author":"FV Brasileiro","year":"2001","unstructured":"Brasileiro, F.V., Greve, F., Most\u00e9faoui, A., Raynal, M.: Consensus in one communication step PaCT. LNCS 2127, 42\u201350 (2001)","journal-title":"LNCS"},{"key":"11_CR20","unstructured":"Buchman, E.: Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Master\u2019s thesis, University of Guelph (2016). http:\/\/hdl.handle.net\/10214\/9769"},{"key":"11_CR21","unstructured":"Buchman, E., Kwon, J.: Cosmos whitepaper: a network of distributed ledgers (2018). https:\/\/cosmos.network\/resources\/whitepaper"},{"key":"11_CR22","unstructured":"Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on BFT consensus. arXiv preprint arXiv:1807.04938 (2018). https:\/\/arxiv.org\/abs\/1807.04938"},{"key":"11_CR23","unstructured":"Buterin, V.: A next-generation smart contract and decentralized application platform (2014)"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Cavada, R., et al.: The NUXMV symbolic model checker, In: CAV. pp. 334\u2013342 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"2","key":"11_CR25","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"},{"issue":"2","key":"11_CR26","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. JACM 43(2), 225\u2013267 (1996)","journal-title":"JACM"},{"issue":"1","key":"11_CR27","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."},{"issue":"5","key":"11_CR28","doi-asserted-by":"publisher","first-page":"912","DOI":"10.1145\/355483.355489","volume":"47","author":"S Chaudhuri","year":"2000","unstructured":"Chaudhuri, S., Herlihy, M., Lynch, N.A., Tuttle, M.R.: Tight Bounds for k-set Agreement. J. ACM 47(5), 912\u2013943 (2000)","journal-title":"J. ACM"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Damian, A., Dr\u0103goi, C., Militaru, A., Widder, J.: Communication-closed asynchronous protocols, In: CAV. pp. 344\u2013363 (2019)","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Decker, C., Seidel, J., Wattenhofer, R.: Bitcoin meets strong consistency, In: ICDCN. pp. 13:1\u201313:10 (2016). https:\/\/doi.org\/10.1145\/2833312.2833321","DOI":"10.1145\/2833312.2833321"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almost-synchronous reductions, In: OOPSLA, pp. 709\u2013725 (2014)","DOI":"10.1145\/2714064.2660211"},{"key":"11_CR32","unstructured":"Dobre, D., Suri, N.: One-step consensus with zero-degradation, In: DSN. pp. 137\u2013146 (2006)"},{"key":"11_CR33","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/7531.7533","volume":"34","author":"D Dolev","year":"1987","unstructured":"Dolev, D., Dwork, C., Stockmeyer, L.: On the minimal synchronism needed for distributed consensus. J. ACM 34, 77\u201397 (1987)","journal-title":"J. ACM"},{"key":"11_CR34","first-page":"161","volume":"8318","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 VMCAI. LNCS 8318, 161\u2013181 (2014)","journal-title":"LNCS"},{"issue":"2","key":"11_CR35","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. J. ACM 35(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"issue":"3","key":"11_CR36","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":"11_CR37","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings, In: POPL, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"issue":"2","key":"11_CR38","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J Esparza","year":"1997","unstructured":"Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85\u2013107 (1997)","journal-title":"Acta Informatica"},{"issue":"2","key":"11_CR39","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"11_CR40","unstructured":"Gleissenthall, K.V., G\u00f6khan Kici, R., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony. In: POPL (2019), (to appear)"},{"key":"11_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-07317-0_4","volume-title":"Formal Methods for Executable Software Models","author":"A Gmeiner","year":"2014","unstructured":"Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 122\u2013171. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_4"},{"issue":"1","key":"11_CR42","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s446-002-8027-4","volume":"15","author":"R Guerraoui","year":"2002","unstructured":"Guerraoui, R.: Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distrib. Comput. 15(1), 17\u201325 (2002)","journal-title":"Distrib. Comput."},{"key":"11_CR43","unstructured":"Hadzilacos, V., Toueg, S.: Fault-tolerant broadcasts and related problems. In: Mullender, S. (ed.) Distributed systems (2nd Ed.) pp. 97\u2013145 (1993)"},{"issue":"7","key":"11_CR44","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":"11_CR45","volume-title":"The SPIN Model Checker","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2003)"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Counter attack on byzantine generals: parameterized model checking of fault-tolerant distributed algorithms, October 2012. http:\/\/arxiv.org\/abs\/1210.3846","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction, In: FMCAD. pp. 201\u2013209 (2013)","DOI":"10.1007\/978-3-642-39176-7_14"},{"key":"11_CR48","first-page":"123:1","volume":"3(OOPSLA)","author":"I Konnov","year":"2019","unstructured":"Konnov, I., Kukovec, J., Tran, T.: TLA+ model checking made symbolic. PACMPL 3(OOPSLA), 123:1\u2013123:30 (2019)","journal-title":"PACMPL"},{"issue":"2","key":"11_CR49","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/s10703-017-0297-4","volume":"51","author":"I Konnov","year":"2017","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: Para$$^2$$: Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods Syst. Des. 51(2), 270\u2013307 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"Konnov, I., Lazi\u0107, 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":"11_CR51","first-page":"125","volume":"8704","author":"I Konnov","year":"2014","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. CONCUR. LNCS 8704, 125\u2013140 (2014)","journal-title":"CONCUR. LNCS"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: CAV (Part I). LNCS, vol. 9206, pp. 85\u2013102 (2015)","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-319-41579-6_2","volume-title":"Perspectives of System Informatics","author":"I Konnov","year":"2016","unstructured":"Konnov, I., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Mazzara, M., Voronkov, A. (eds.) PSI 2015. LNCS, vol. 9609, pp. 6\u201321. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41579-6_2"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03424-5","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems","year":"2018","unstructured":"Margaria, T., Steffen, B. (eds.): ISoLA 2018. LNCS, vol. 11246. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5"},{"key":"11_CR55","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"IV Konnov","year":"2017","unstructured":"Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017)","journal-title":"Inf. Comput."},{"key":"11_CR56","unstructured":"Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR. pp. 21:1\u201321:17 (2018)"},{"key":"11_CR57","unstructured":"Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR. LIPIcs, vol. 118, pp. 19:1\u201319:17 (2018)"},{"issue":"7","key":"11_CR58","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"11_CR59","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"11_CR60","doi-asserted-by":"publisher","unstructured":"Lazi\u0107, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: OPODIS. LIPIcs, vol. 95, pp. 32:1\u201332:20 (2017). https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2017.32","DOI":"10.4230\/LIPIcs.OPODIS.2017.32"},{"key":"11_CR61","unstructured":"Le Lann, G.: Distributed systems - towards a formal approach. In: IFIP Congress, pp. 155\u2013160 (1977). http:\/\/www-roc.inria.fr\/novaltis\/publications\/IFIP%20Congress%201977.pdf"},{"key":"11_CR62","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Rushby, J.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: FTCS, pp. 402\u2013411 (1993)","DOI":"10.1007\/3-540-56922-7_24"},{"key":"11_CR63","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"11_CR64","unstructured":"Malekpour, M.R., Siminiceanu, R.: Comments on the \u201cByzantine self-stabilizing pulse synchronization\u201d. protocol: Counterexamples. Tech. rep., NASA, February 2006. http:\/\/shemesh.larc.nasa.gov\/fm\/papers\/Malekpour-2006-tm213951.pdf"},{"key":"11_CR65","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/j.tcs.2017.03.018","volume":"709","author":"A Most\u00e9faoui","year":"2018","unstructured":"Most\u00e9faoui, A., Moumen, H., Raynal, M.: Randomized k-set agreement in crash-prone and Byzantine asynchronous systems. Theor. Comput. Sci. 709, 80\u201397 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR66","unstructured":"Most\u00e9faoui, A., Mourgaya, E., Parv\u00e9dy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: DSN, pp. 541\u2013550 (2003)"},{"key":"11_CR67","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"11_CR68","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"11_CR69","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"},{"issue":"2","key":"11_CR70","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"MC Pease","year":"1980","unstructured":"Pease, M.C., Shostak, R.E., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"11_CR71","unstructured":"Raynal, M.: A case study of agreement problems in distributed systems: Non-blocking atomic commitment. In: HASE, pp. 209\u2013214 (1997)"},{"key":"11_CR72","doi-asserted-by":"crossref","unstructured":"Raynal, M.: Fault-tolerant agreement in synchronous message-passing systems. Morgan & Claypool Publishers, Synthesis Lectures on Distributed Computing Theory (2010)","DOI":"10.1007\/978-3-031-02001-8"},{"issue":"4","key":"11_CR73","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/98163.98167","volume":"22","author":"FB Schneider","year":"1990","unstructured":"Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv. 22(4), 299\u2013319 (1990)","journal-title":"ACM Comput. Surv."},{"key":"11_CR74","first-page":"281","volume":"2(POPL)","author":"I Sergey","year":"2018","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 281\u20132830 (2018)","journal-title":"PACMPL"},{"key":"11_CR75","first-page":"438","volume":"5218","author":"YJ Song","year":"2008","unstructured":"Song, Y.J., van Renesse, R.: Bosco: one-step Byzantine asynchronous consensus. DISC. LNCS 5218, 438\u2013450 (2008)","journal-title":"DISC. LNCS"},{"issue":"3","key":"11_CR76","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Optimal clock synchronization. J. ACM 34(3), 626\u2013645 (1987)","journal-title":"J. ACM"},{"key":"11_CR77","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T Srikanth","year":"1987","unstructured":"Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Dist. Comp. 2, 80\u201394 (1987)","journal-title":"Dist. Comp."},{"key":"11_CR78","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. LNCS, vol. 11428, pp. 357\u2013374. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_20"},{"issue":"4","key":"11_CR79","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"key":"11_CR80","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":"11_CR81","doi-asserted-by":"crossref","unstructured":"Yin, M., Malkhi, D., Reiter, M.K., Golan-Gueta, G., Abraham, I.: Hotstuff: BFT consensus with linearity and responsiveness. In: PODC, pp. 347\u2013356 (2019)","DOI":"10.1145\/3293611.3331591"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-50086-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,8]],"date-time":"2024-06-08T23:02:31Z","timestamp":1717887751000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-50086-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030500856","9783030500863"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-50086-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 June 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"40","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2020\/forte","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"25","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":"10","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":"1","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":"40% - 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":"3","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}