{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T23:07:15Z","timestamp":1760828835408},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001416"},{"type":"electronic","value":"9783540361350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36135-9_13","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:43:21Z","timestamp":1180665801000},"page":"194-209","source":"Crossref","is-referenced-by-count":15,"title":["Verifying Randomized Byzantine Agreement_"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/3-540-44618-4_24","volume-title":"Reasoning about probabilistic lossy channel systems","author":"P. Abdulla","year":"2000","unstructured":"P. Abdulla, C. Baier, P. Iyer, and B. Jonsson. Reasoning about probabilistic lossy channel systems. In Proc. CONCUR\u201900, volume 1877 of LNCS, pages 320\u2013333. Springer, 2000."},{"issue":"3","key":"13_CR2","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J. Aspnes","year":"1990","unstructured":"J. Aspnes and M. Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms, 11(3):441\u2013460, 1990.","journal-title":"Journal of Algorithms"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"C. Cachin. Distributing trust on the Internet. In Proc. DSN\u201901, pages 183\u2013192. IEEE Computer Society Press, 2001.","DOI":"10.1109\/DSN.2001.941404"},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1007\/3-540-44647-8_31","volume-title":"Secure and efficient asynchronous broadcast protocols (extended abstract)","author":"C. Cachin","year":"2001","unstructured":"C. Cachin, K. Kursawe, F. Petzold, and V. Shoup. Secure and efficient asynchronous broadcast protocols (extended abstract). In Proc. CRYPTO 2001, volume 2139 of LNCS, pages 524\u2013541. Springer, 2001."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"C. Cachin, K. Kursawe, and V. Shoup. Random oracles in Constantinople: practical asynchronous Byzantine agreement using cryptography (extended abstract). In Proc. PODC\u201900, pages 123\u2013132. ACM Press, 2000.","DOI":"10.1145\/343477.343531"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"C. Cachin and J. Poritz. Secure intrusion-tolerant replication on the Internet. In Proc. DSN-2002, pages 167\u2013176. IEEE Computer Society Press, 2002.","DOI":"10.1109\/DSN.2002.1028897"},{"key":"13_CR7","unstructured":"M. Castro and B. Liskov. Practical Byzantine fault tolerance. In Proc. ACM Symp. on Operating Systems Design and Implementation (OSDI), pages 173\u2013186, 1999."},{"key":"13_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Reachability analysis of probabilistic systems by successive refinements","author":"P. D\u2019Argenio","year":"2001","unstructured":"P. D\u2019Argenio, B. Jeannet, H. Jensen, and K. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Proc. PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 39\u201356. Springer, 2001."},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-44685-0_24","volume-title":"Compositional methods for probabilistic systems","author":"L. Alfaro de","year":"2001","unstructured":"L. de Alfaro, T. Henzinger, and R. Jhala. Compositional methods for probabilistic systems. In Proc. CONCUR\u201901, volume 2154 of LNCS, pages 351\u2013365. Springer, 2001."},{"issue":"5","key":"13_CR10","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M. Fischer","year":"1985","unstructured":"M. Fischer, N. Lynch, and M. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(5):374\u2013382, 1985.","journal-title":"Journal of the ACM"},{"key":"13_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/3-540-44804-7_5","volume-title":"Coin lemmas with random variables","author":"K. Folegati","year":"2001","unstructured":"K. Folegati and R. Segala. Coin lemmas with random variables. In Proc. PAPMPROBMIV\u2019 01, volume 2165 of LNCS, pages 71\u201386. Springer, 2001."},{"key":"13_CR12","unstructured":"J. Hurd. Verification of the Miller-Rabin probabilistic primality test. In Proc. TPHOLs\u201901, number EDI-INF-RR-0046 in Informatics Report Series, pages 223\u2013238. Division of Informatics, University of Edinburgh, 2001."},{"key":"13_CR13","unstructured":"M. Kwiatkowska and G. Norman. Automated verification of a randomized Byzantine agreement protocol. Technical Report CSR-01-11, University of Birmingham, School of Computer Science, 2001."},{"key":"13_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Probabilistic symbolic model checking with PRISM: A hybrid approach","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS\u201902, volume 2280 of LNCS, pages 52\u201367. Springer, 2002."},{"key":"13_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Automated verification of a randomized distributed consensus algorithm using Cadence SMV and PRISM","author":"M. Kwiatkowska","year":"2001","unstructured":"M. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus algorithm using Cadence SMV and PRISM. In Proc. CAV\u201901, volume 2102 of LNCS, pages 194\u2013206. Springer, 2001."},{"key":"13_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44685-0_12","volume-title":"Symbolic computation of maximal probabilistic reachability","author":"M. Kwiatkowska","year":"2001","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston. Symbolic computation of maximal probabilistic reachability. In Proc. CONCUR\u201901, volume 2154 of LNCS, pages 169\u2013183. Springer, 2001."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE1394 Firewire root contention. Special Issue of Formal Aspects of Computing, 2002. To appear.","DOI":"10.1007\/s001650300007"},{"issue":"1\u20133","key":"13_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K. McMillan","year":"2000","unstructured":"K. McMillan. A methodology for hardware verification using compositional model checking. Science of Computer Programming, 37(1\u20133):279\u2013309, 2000.","journal-title":"Science of Computer Programming"},{"key":"13_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/10722167_25","volume-title":"Induction and compositional model checking","author":"K. McMillan","year":"2000","unstructured":"K. McMillan, S. Qadeer, and J. Saxe. Induction and compositional model checking. In Proc. CAV\u201900, volume 1855 of LNCS, pages 312\u2013327, 2000."},{"issue":"3","key":"13_CR20","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/PL00008917","volume":"13","author":"A. Pogosyants","year":"2000","unstructured":"A. Pogosyants, R. Segala, and N. Lynch. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing, 13(3):155\u2013186, 2000.","journal-title":"Distributed Computing"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"M. Rabin. Randomized Byzantine generals. In Proc. FOCS\u201983, pages 403\u2013409. IEEE Computer Society Press, 1983.","DOI":"10.1109\/SFCS.1983.48"},{"key":"13_CR22","unstructured":"A. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997."},{"key":"13_CR23","unstructured":"R. Segala. Modelling and Verifiation of Randomized Distributed Real Time Systems. PhDthesis, Massachusetts Institute of Technology, 1995."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"R. Segala. The essence of coin lemmas. In Proc. PROBMIV\u201998, volume 22 of ENTCS, 1998.","DOI":"10.1016\/S1571-0661(05)80603-6"},{"key":"13_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-45539-6_15","volume-title":"Practical threshold signatures","author":"V. Shoup","year":"2000","unstructured":"V. Shoup. Practical threshold signatures. In Proc. Eurocrypt 2000, volume 1807 of LNCS, pages 207\u2013220. Springer, 2000."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36135-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:17:43Z","timestamp":1556464663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36135-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001416","9783540361350"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-36135-9_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}