{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:17:48Z","timestamp":1749010668457,"version":"3.41.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415789"},{"type":"electronic","value":"9783319415796"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41579-6_2","type":"book-chapter","created":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T02:44:48Z","timestamp":1466995488000},"page":"6-21","source":"Crossref","is-referenced-by-count":9,"title":["What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","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":[[2016,6,28]]},"reference":[{"issue":"1\/2","key":"2_CR1","first-page":"29","volume":"8","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8(1\/2), 29\u201361 (2012)","journal-title":"JSAT"},{"key":"2_CR2","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed Computing","author":"H Attiya","year":"2004","unstructured":"Attiya, H., Welch, J.: Distributed Computing, 2nd edn. Wiley, New York (2004)","edition":"2"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"2_CR4","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015)"},{"issue":"4","key":"2_CR5","doi-asserted-by":"crossref","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":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-44743-1_4","volume-title":"Parallel Computing Technologies","author":"F Brasileiro","year":"2001","unstructured":"Brasileiro, F., Greve, F.G.P., Most\u00e9faoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V.E. (ed.) PaCT 2001. LNCS, vol. 2127, pp. 42\u201350. Springer, Heidelberg (2001)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, heidelberg (2014)"},{"issue":"2","key":"2_CR8","doi-asserted-by":"crossref","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"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"issue":"5","key":"2_CR10","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Dobre, D., Suri, N.: One-step consensus with zero-degradation. In: DSN, pp. 137\u2013146 (2006)","DOI":"10.1109\/DSN.2006.55"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"2","key":"2_CR14","doi-asserted-by":"crossref","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":"2","key":"2_CR15","doi-asserted-by":"crossref","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":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"issue":"1","key":"2_CR17","doi-asserted-by":"crossref","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":"2_CR18","volume-title":"The SPIN Model Checker","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2003)"},{"key":"2_CR19","unstructured":"Imbs, D., Raynal, M.: Simple and efficient reliable broadcast in the presence of Byzantine processes. CoRR abs\/1510.06882 (2015). http:\/\/arxiv.org\/abs\/1510.06882"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: PODC, pp. 119\u2013121 (2013)","DOI":"10.1145\/2484239.2484285"},{"key":"2_CR21","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.1109\/FMCAD.2013.6679411"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-642-39176-7_14","volume-title":"Model Checking Software","author":"A John","year":"2013","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209\u2013226. Springer, Heidelberg (2013)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-662-44584-6_10","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"I Konnov","year":"2014","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed\u00a0algorithms: reachability. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 125\u2013140. Springer, Heidelberg (2014)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-21690-4_6","volume-title":"Computer Aided Verification","author":"I Konnov","year":"2015","unstructured":"Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of\u00a0threshold-based distributed algorithms. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 85\u2013102. Springer, Heidelberg (2015)"},{"issue":"2","key":"2_CR25","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (1998)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"4","key":"2_CR26","first-page":"18","volume":"32","author":"L Lamport","year":"2001","unstructured":"Lamport, L.: Paxos made simple. ACM SIGACT News 32(4), 18\u201325 (2001)","journal-title":"ACM SIGACT News"},{"key":"2_CR27","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 Longman Publishing Co., Inc., Boston (2002)"},{"key":"2_CR28","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"2_CR29","doi-asserted-by":"crossref","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)","DOI":"10.1109\/DSN.2003.1209964"},{"key":"2_CR30","unstructured":"Netflix: 5 lessons we have learned using AWS (2010). http:\/\/techblog.netflix.com\/2010\/12\/5-lessons-weve-learned-using-aws.html"},{"issue":"2","key":"2_CR31","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with $${(0,1,\\infty )}$$ -counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: HASE, pp. 209\u2013214 (1997)","DOI":"10.1109\/HASE.1997.648067"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","first-page":"438","volume-title":"Distributed Computing","author":"YJ Song","year":"2008","unstructured":"Song, Y.J., van Renesse, R.: Bosco: one-step byzantine asynchronous consensus. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 438\u2013450. Springer, Heidelberg (2008)"},{"key":"2_CR35","doi-asserted-by":"crossref","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."}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41579-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T22:51:04Z","timestamp":1748991064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41579-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415789","9783319415796"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41579-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}