{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T01:13:55Z","timestamp":1768353235723,"version":"3.49.0"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633893","type":"print"},{"value":"9783319633909","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_12","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"217-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Cutoff Bounds for Consensus Algorithms"],"prefix":"10.1007","author":[{"given":"Ognjen","family":"Mari\u0107","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf., pp. 1\u201322 (2015)","DOI":"10.1007\/s10009-015-0406-x"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10009-011-0216-8","volume":"14","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A.: Regular model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 109\u2013118 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR4","unstructured":"Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the \u201csmall scope hypothesis\u201d. In: POPL, vol. 2 (2003)"},{"issue":"6","key":"12_CR5","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"issue":"7","key":"12_CR6","doi-asserted-by":"crossref","first-page":"20:20","DOI":"10.1145\/2639988.2655736","volume":"12","author":"P Bailis","year":"2014","unstructured":"Bailis, P., Kingsbury, K.: The network is reliable. ACM Queue 12(7), 20:20\u201320:32 (2014)","journal-title":"ACM Queue"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice: completely asynchronous agreement protocols. In: PODC, pp. 27\u201330 (1983)","DOI":"10.1145\/800221.806707"},{"issue":"2","key":"12_CR8","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 (JACM) 43(2), 225\u2013267 (1996)","journal-title":"J. ACM (JACM)"},{"key":"12_CR9","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). doi:10.1007\/978-3-642-04420-5_10"},{"issue":"1","key":"12_CR10","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":"12_CR11","unstructured":"Debrat, H., Merz, S.: Verifying fault-tolerant distributed algorithms in the heard-of model. Archive of Formal Proofs (AFP) (2012). https:\/\/www.isa-afp.org\/entries\/Heard_Of.shtml"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"131","DOI":"10.4204\/EPTCS.161.13","volume":"161","author":"G Delzanno","year":"2014","unstructured":"Delzanno, G., Tatarek, M., Traverso, R.: Model Checking Paxos in Spin. Electron. Proc. Theoret. Comput. Sci. 161, 131\u2013146 (2014)","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"12_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). doi:10.1007\/978-3-642-54013-4_10"},{"key":"12_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"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"EA Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000). doi:10.1007\/10721959_19"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 247\u2013262. Springer, Heidelberg (2003). doi:10.1007\/978-3-540-39724-3_22"},{"issue":"04","key":"12_CR17","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(04), 527\u2013549 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"2","key":"12_CR18","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":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-78800-3_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Fisman","year":"2008","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 315\u2013331. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_22"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Jobstmann, B., Singh, V.: Model checking transactional memories. In: PLDI, pp. 372\u2013382 (2008)","DOI":"10.1145\/1379022.1375626"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: proving practical distributed systems correct. In SOSP, pp. 1\u201317 (2015)","DOI":"10.1145\/2815400.2815428"},{"issue":"1","key":"12_CR22","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR23","volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Hutle, M., Schiper, A.: Communication predicates: a high-level abstraction for coping with transient and dynamic faults. In: 37th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, 2007, DSN 2007, pp. 92\u2013101. IEEE (2007)","DOI":"10.1109\/DSN.2007.25"},{"key":"12_CR25","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"issue":"7","key":"12_CR26","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1109\/32.538605","volume":"22","author":"D Jackson","year":"1996","unstructured":"Jackson, D., Damon, C.A.: Elements of style: analyzing a software design feature with a counterexample detector. IEEE Trans. Softw. Eng. 22(7), 484\u2013495 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR27","unstructured":"Jaskelioff, M., Merz, S.: Proving the correctness of Disk Paxos. Archive of Formal Proofs (AFP) (2005). https:\/\/www.isa-afp.org\/entries\/DiskPaxos.shtml"},{"key":"12_CR28","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":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-30793-5_2","volume-title":"Formal Techniques for Distributed Systems","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-30793-5_2"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_55"},{"key":"12_CR31","unstructured":"Kingsbury, K.: Jepsen: Testing the Partition Tolerance of PostgreSQL, Redis, MongoDB and Riak (2013). http:\/\/www.infoq.com\/articles\/jepsen"},{"key":"12_CR32","volume-title":"The Art of Computer Programming, Vol III: Sorting and Searching","author":"DE Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming, Vol III: Sorting and Searching. Addison-Wesley, Boston (1973)"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi:10.1007\/978-3-662-44584-6_10"},{"key":"12_CR34","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: Computer Aided Verification, pp. 85\u2013102, July 2015","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-33475-7_15","volume-title":"Theoretical Computer Science","author":"P K\u00fcfner","year":"2012","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33475-7_15"},{"issue":"2","key":"12_CR36","doi-asserted-by":"publisher","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."},{"key":"12_CR37","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations part I: untimed systems. Inf. Comput. 121, 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Consensus Refined. In: DSN, pp. 391\u2013402 (2015)","DOI":"10.1109\/DSN.2015.38"},{"key":"12_CR39","unstructured":"Mari\u0107, O.: Formal Verification of Fault-Tolerant Systems. Ph.D. thesis, Department of Computer Science, ETH Zurich (2017). http:\/\/dx.doi.org\/10.3929\/ethz-a-010892776"},{"key":"12_CR40","unstructured":"Mari\u0107, O.: The Consensus Verifier, May 2017. http:\/\/www.infsec.ethz.ch\/research\/software\/consl-verifier"},{"key":"12_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-662-43652-3_3","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014","author":"C Newcombe","year":"2014","unstructured":"Newcombe, C.: Why Amazon Chose TLA$$^+$$. In: Ait, A.Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. LNCS, vol. 8477, pp. 25\u201339. Springer, Berlin (2014)"},{"key":"12_CR42","unstructured":"Oetsch, J., Prischink, M., P\u00fchrer, J., Schwengerer, M., Tompits, H.: On the small-scope hypothesis for testing answer-set programs. In: KR (2012)"},{"key":"12_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/BFb0028994","volume-title":"STACS 89","author":"N Santoro","year":"1989","unstructured":"Santoro, N., Widmayer, P.: Time is not a healer. In: Monien, B., Cori, R. (eds.) STACS 1989. LNCS, vol. 349, pp. 304\u2013313. Springer, Heidelberg (1989). doi:10.1007\/BFb0028994"},{"key":"12_CR44","doi-asserted-by":"crossref","unstructured":"Schiper, N., Rahli, V., van Renesse, R., Bickford, M., Constable, R.: Developing correctly replicated databases using formal tools. In: DSN, pp. 395\u2013406 (2014)","DOI":"10.1109\/DSN.2014.45"},{"issue":"4","key":"12_CR45","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":"12_CR46","doi-asserted-by":"crossref","unstructured":"Tsuchiya, T., Schiper, A.: Model checking of consensus algorithms. In: SRDS, pp. 137\u2013148, October 2007","DOI":"10.1109\/SRDS.2007.20"},{"key":"12_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-540-87779-0_32","volume-title":"Distributed Computing","author":"T Tsuchiya","year":"2008","unstructured":"Tsuchiya, T., Schiper, A.: Using bounded model checking to verify consensus algorithms. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 466\u2013480. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-87779-0_32"},{"issue":"5\u20136","key":"12_CR48","first-page":"341","volume":"23","author":"T Tsuchiya","year":"2010","unstructured":"Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrib. Comput. 23(5\u20136), 341\u2013358 (2010)","journal-title":"Distrib. Comput."},{"key":"12_CR49","unstructured":"Yuan, D., Luo, Y., Zhuang, X., Rodrigues, G.R., Zhao, X., Zhang, Y., Jain, P.U., Stumm, M.: Simple testing can prevent most critical failures: an analysis of production failures in distributed dataintensive systems. In: OSDI (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T01:07:53Z","timestamp":1750554473000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","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":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}