{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:52:02Z","timestamp":1754488322760},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569220"},{"type":"electronic","value":"9783540477877"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56922-7_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:54:19Z","timestamp":1330257259000},"page":"292-304","source":"Crossref","is-referenced-by-count":18,"title":["The formal verification of an algorithm for interactive consistency under a hybrid fault model"],"prefix":"10.1007","author":[{"given":"Patrick","family":"Lincoln","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Rushby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"issue":"6A","key":"24_CR1","doi-asserted-by":"crossref","first-page":"755","DOI":"10.1007\/BF03180571","volume":"4","author":"William R. R. Bevier","year":"1992","unstructured":"William R. Bevier and William D. Young. Machine checked proofs of the design of a fault-tolerant circuit. Formal Aspects of Computing, 4(6A):755\u2013775, 1992.","journal-title":"Formal Aspects of Computing"},{"key":"24_CR2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/978-94-011-3488-0_5","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe, volume 1 of Automated Reasoning Series","author":"Robert S. S. Boyer","year":"1991","unstructured":"Robert S. Boyer and J Strother Moore. MJRTY\u2014a fast majority vote algorithm. In Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, volume 1 of Automated Reasoning Series, pages 105\u2013117. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1991."},{"key":"24_CR3","first-page":"522","volume-title":"Protocol verification as a hardware design aid","author":"David L. L. Dill","year":"1992","unstructured":"David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522\u2013525. IEEE Computer Society, 1992. Cambridge, MA, October 11\u201314."},{"issue":"3","key":"24_CR4","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382\u2013401, July 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR5","volume-title":"Technical Report SRI-CSL-93-02","author":"P. Lincoln","year":"1993","unstructured":"Patrick Lincoln and John Rushby. Formal verification of an algorithm for interactive consistency under a hybrid fault model. Technical Report SRI-CSL-93-02, Computer Science Laboratory, SRI International, Menlo Park, CA, March 1993."},{"key":"24_CR6","volume-title":"Fault Tolerant Computing Symposium 23","author":"P. Lincoln","year":"1993","unstructured":"Patrick Lincoln and John Rushby. A formally verified algorithm for interactive consistency under a hybrid fault model. In Fault Tolerant Computing Symposium 23, Toulouse, France, June 1993. IEEE Computer Society. To appear."},{"key":"24_CR7","volume-title":"NASA Technical Paper 2857","author":"Dale A. A. Mackall","year":"1988","unstructured":"Dale A. Mackall. Development and flight test experiences with a flight-crucial digital control system. NASA Technical Paper 2857, NASA Ames Research Center, Dryden Flight Research Facility, Edwards, CA, 1988."},{"key":"24_CR8","first-page":"748","volume-title":"11th International Conference on Automated Deduction (CADE)","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748\u2013752, Saratoga, NY, June 1992. Volume 607 of Lecture Notes in Artificial Intelligence, Springer Verlag."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Some lessons learned. In Formal Methods Europe '93, Odense, Denmark, April 1993. Springer Verlag Lecture Notes in Computer Science. To appear.","DOI":"10.1007\/BFb0024663"},{"issue":"2","key":"24_CR10","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M. Pease","year":"1980","unstructured":"M. Pease, R. Shostak, and L. Lamport. Reaching agreement in the presence of faults. Journal of the ACM, 27(2):228\u2013234, April 1980.","journal-title":"Journal of the ACM"},{"key":"24_CR11","volume-title":"Technical Report SRI-CSL-92-1","author":"J. Rushby","year":"1992","unstructured":"John Rushby. Formal verification of an Oral Messages algorithm for interactive consistency. Technical Report SRI-CSL-92-1, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1992. Also available as NASA Contractor Report 189704, October 1992."},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"John Rushby and Friedrich von Henke. Formal verification of algorithms for critical systems. In SIGSOFT '91: Software for Critical Systems, pages 1\u201315, New Orleans, LA, December 1991. Expanded version to appear in IEEE Transactions on Software Engineering, 1993.","DOI":"10.1109\/32.210304"},{"key":"24_CR13","series-title":"Volume 571 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-55092-5_12","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"N. Shankar","year":"1992","unstructured":"Natarajan Shankar. Mechanical verification of a generalized protocol for Byzantine fault-tolerant clock synchronization. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 217\u2013236, Nijmegen, The Netherlands, January 1992. Volume 571 of Lecture Notes in Computer Science, Springer Verlag."},{"key":"24_CR14","first-page":"93","volume-title":"Interactive consistency with multiple failure modes","author":"P. Thambidurai","year":"1988","unstructured":"Philip Thambidurai and You-Keun Park. Interactive consistency with multiple failure modes. In 7th Symposium on Reliable Distributed Systems, pages 93\u2013100, Columbus, OH, October 1988. IEEE Computer Society."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56922-7_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:57:34Z","timestamp":1619571454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56922-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569220","9783540477877"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-56922-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}