{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T23:07:24Z","timestamp":1760828844474},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_17","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"194-206","source":"Crossref","is-referenced-by-count":33,"title":["Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Segala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"issue":"3","key":"17_CR1","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":"17_CR2","doi-asserted-by":"crossref","unstructured":"C. Baier, E. Clarke, and V. Hartonas-Garmhausen. On the semantic foundations of Probabilistic VERUS. In C. Baier, M. Huth, M. Kwiatkowska, and M. Ryan, editors, Proc. PROBMIV\u201998, volume 22 of ENTCS, 1998.","DOI":"10.1016\/S1571-0661(05)80594-8"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125\u2013155, 1998.","journal-title":"Distributed Computing"},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Model checking of probabilistic and nondeterministic systems","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. Thiagarajan, editor, Proc. FST & TCS, volume 1026 of LNCS, pages 499\u2013513, 1995."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"C. Cachin, K. Kursawe, and V. Shoup. Random oracles in Constantinople: Practical asynchronous byzantine agreement using cryptography. In Proc. PODC\u201900, pages 123\u2013132, 2000.","DOI":"10.1145\/343477.343531"},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Symbolic model checking of concurrent probabilistic systems using MTBDDs and the Kronecker representation","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic systems using MTBDDs and the Kronecker representation. In S. Graf and M. Schwartzbach, editors, Proc. TACAS\u20192000, volume 1785 of LNCS, pages 395\u2013410, 2000."},{"issue":"5","key":"17_CR7","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 commit with one faulty process. Journal of the ACM, 32(5):374\u2013382, 1985.","journal-title":"Journal of the ACM"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(4):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"A Markov Chain Model Checker","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov Chain Model Checker. In S. Graf and M. Schwartzbach, editors, Proc. TACAS 2000, volume 1785 of LNCS, pages 347\u2013362, 2000."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"A. Itai and M. Rodeh. The lord of the ring or probabilistic methods for breaking symmetry in distributed networks. Technical Report RJ 3110, IBM, 1981.","DOI":"10.1109\/SFCS.1981.41"},{"key":"17_CR11","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Verfication of an implementation of Tomasulo\u2019s algorithm by compositional model checking","author":"K. McMillan","year":"1998","unstructured":"K. McMillan. Verfication of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In A. Hu and M. Vardi, editors, Proc. CAV\u201998, volume 1427 of LNCS, pages 110\u2013121, 1998."},{"key":"17_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Verification of infinite state systems by compositional model checking","author":"K. McMillan","year":"1999","unstructured":"K. McMillan. Verification of infinite state systems by compositional model checking. In L. Pierre and T. Kropf, editors, Proc. CHARME\u201999, volume 1703 of LNCS, pages 219\u2013233, 1999."},{"key":"17_CR14","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 E. Emerson and A. P. Sistla, editors, Proc. CAV 2000, volume 1855 of LNCS, pages 312\u2013327, 2000."},{"issue":"3","key":"17_CR15","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":"17_CR16","volume-title":"Public software","author":"F. Somenzi","year":"1997","unstructured":"F. Somenzi. CUDD: CU decision diagram package. Public software, Colorado University, Boulder, 1997."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Proc. FOCS\u201985, pages 327\u2013338, 1985.","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T16:10:25Z","timestamp":1634919025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}