{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:03Z","timestamp":1763468043155},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642245497"},{"type":"electronic","value":"9783642245503"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24550-3_11","type":"book-chapter","created":{"date-parts":[[2011,10,8]],"date-time":"2011-10-08T06:56:37Z","timestamp":1318056997000},"page":"120-134","source":"Crossref","is-referenced-by-count":16,"title":["Formal Verification of Consensus Algorithms Tolerating Malicious Faults"],"prefix":"10.1007","author":[{"given":"Bernadette","family":"Charron-Bost","sequence":"first","affiliation":[]},{"given":"Henri","family":"Debrat","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bar-noy, A., Dolev, D., Dwork, C., Strong, H.R.: Shifting gears: Changing algorithms on the fly to expedite Byzantine agreement. In: Information and Computation, pp. 42\u201351 (1987)","DOI":"10.1145\/41840.41844"},{"key":"11_CR2","first-page":"244","volume-title":"Proc. 26th Annual ACM Symposium on Principles of Distributed Computing, PODC 2007","author":"M. Biely","year":"2007","unstructured":"Biely, M., Widder, J., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A.: Tolerating corrupted communication. In: Proc. 26th Annual ACM Symposium on Principles of Distributed Computing, PODC 2007, pp. 244\u2013253. ACM, New York (2007)"},{"key":"11_CR3","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.\u00a05797, pp. 93\u2013106. Springer, Heidelberg (2009)"},{"issue":"2-3","key":"11_CR4","first-page":"273","volume":"3","author":"B. Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Merz, S.: Formal verification of a Consensus algorithm in the Heard-Of model. Int. J. Software and Informatics\u00a03(2-3), 273\u2013303 (2009)","journal-title":"Int. J. Software and Informatics"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Charron-Bost, B., Schiper, A.: The Heard-Of model: Computing in distributed systems with benign failures. In: Distributed Computing (2009)","DOI":"10.1007\/s00446-009-0084-6"},{"issue":"2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C. Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N.A., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM\u00a035(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Science Comp. Prog.\u00a02(3) (April 1982)","DOI":"10.1016\/0167-6423(83)90013-8"},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M.J. Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM\u00a032(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"issue":"2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10009-008-0097-7","volume":"11","author":"C. Georgiou","year":"2009","unstructured":"Georgiou, C., Lynch, N.A., Mavrommatis, P., Tauber, J.A.: Automated implementation of complex distributed algorithms specified in the IOA language. Intl. J. Software Tools for Technology Transfer\u00a011(2), 153\u2013171 (2009)","journal-title":"Intl. J. Software Tools for Technology Transfer"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s001650050035","volume":"11","author":"W.H. Hesselink","year":"1999","unstructured":"Hesselink, W.H.: The verified incremental design of a distributed spanning tree algorithm: Extended abstract. Formal Asp. Comput.\u00a011(1), 45\u201355 (1999)","journal-title":"Formal Asp. Comput."},{"key":"11_CR11","unstructured":"Jaskelioff, M., Merz, S.: Proving the correctness of Disk Paxos. Archive of Formal Proofs (2005), http:\/\/afp.sourceforge.net\/entries\/DiskPaxos.shtml"},{"key":"11_CR12","series-title":"IFIP","first-page":"657","volume-title":"Information Processing 1983: Proceedings of the IFIP 9th World Congress","author":"L. Lamport","year":"1983","unstructured":"Lamport, L.: What good is temporal logic? In: Mason, R.E.A. (ed.) Information Processing 1983: Proceedings of the IFIP 9th World Congress, Paris. IFIP, pp. 657\u2013668. North-Holland, Amsterdam (September 1983)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Byzantining Paxos by refinement. Technical report, Microsoft Research (December 2010)","DOI":"10.1007\/978-3-642-24100-0_22"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-58468-4_159","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"L. Lamport","year":"1994","unstructured":"Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, pp. 41\u201376. Springer, Heidelberg (1994)"},{"key":"11_CR15","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"5","key":"11_CR17","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Proc. Letters\u00a063(5), 243\u2013246 (1997)","journal-title":"Inf. Proc. Letters"},{"key":"11_CR18","first-page":"608","volume-title":"22nd Intl. Conf. Distributed Computing Systems (ICDCS 2002)","author":"U. Schmid","year":"2002","unstructured":"Schmid, U., Weiss, B., Rushby, J.M.: Formally verified byzantine agreement in presence of link faults. In: 22nd Intl. Conf. Distributed Computing Systems (ICDCS 2002), Vienna, Austria, pp. 608\u2013616. IEEE Comp. Society, Los Alamitos (2002)"},{"key":"11_CR19","first-page":"137","volume-title":"26th IEEE Symp. Reliable Distributed Systems (SRDS 2007)","author":"T. Tsuchiya","year":"2007","unstructured":"Tsuchiya, T., Schiper, A.: Model checking of consensus algorithms. In: 26th IEEE Symp. Reliable Distributed Systems (SRDS 2007), Beijing, China, pp. 137\u2013148. IEEE Comp. Society, Los Alamitos (2007)"},{"key":"11_CR20","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.\u00a05218, pp. 466\u2013480. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Stabilization, Safety, and Security of Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24550-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T06:54:10Z","timestamp":1560754450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24550-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642245497","9783642245503"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24550-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}