{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T06:34:10Z","timestamp":1770705250490,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540609735","type":"print"},{"value":"9783540497493","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-60973-3_113","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:08:51Z","timestamp":1330290531000},"page":"662-681","source":"Crossref","is-referenced-by-count":68,"title":["Experiments in theorem proving and model checking for protocol verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"issue":"5","key":"37_CR1","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K. A. Bartlett","year":"1969","unstructured":"K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260, 261, May 1969.","journal-title":"Communications of the ACM"},{"key":"37_CR2","unstructured":"Rachel Mary Cardell-Oliver. The formal verification of hard real-time systems. Technical Report 255, University of Cambridge Computer Laboratory, 1992."},{"key":"37_CR3","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"issue":"5","key":"37_CR4","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clark","year":"1994","unstructured":"E.M. Clark, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"37_CR5","unstructured":"C. Comes, J. Courant, J.C. Filliatre, G. Huet, P. Manoury, C Paulin-Mohring, C. Munoz, C. Murthy, C. Parent, A. Saibi, and B. Werner. The Coq proof assistant reference manual, version 5.10. Technical report, INRIA, Rocquencourt, Prance, February 1995. This version is newer than the version used to verify the BRP-protocol in [10]."},{"key":"37_CR6","series-title":"volume 910 of Lecture Notes in Computer Science","first-page":"203","volume-title":"Theorem Provers in Circuit Design (TPCD '94)","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design (TPCD '94), volume 910 of Lecture Notes in Computer Science, pages 203\u2013222, Bad Herrenalb, Germany, September 1994. Springer-Verlag."},{"key":"37_CR7","unstructured":"Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL*, \u2203CTL* and CTL*. In Ernst-R\u00fcdiger Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET '94), pages 561\u2013581, 1994."},{"key":"37_CR8","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. J. C. C. Gordon","year":"1988","unstructured":"M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128. Kluwer, Dordrecht, The Netherlands, 1988."},{"key":"37_CR9","unstructured":"J. F. Groote and J. C. van de Pol. A bounded retransmission protocol for large packets. A case study in computer checked verification. Logic Group Preprint Series 100, Utrecht University, 1993."},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-R9420, Centrum voor Wiskunde en Informatica (CWI), Computer Science\/Department of Software Technology, March 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"37_CR11","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991."},{"key":"37_CR12","volume-title":"ROBDD software. Department of Electrical Engineering","author":"G. Janssen","year":"1993","unstructured":"G. Janssen. ROBDD software. Department of Electrical Engineering, Eindhoven University of Technology, October 1993."},{"issue":"4","key":"37_CR13","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"SE-10","author":"Simon S. S. Lam","year":"1984","unstructured":"Simon S. Lam and A. Udaya Shankar. Protocol verification via projections. IEEE Trans. on S.W. Engg, SE-10(4):325\u2013342, July 1984.","journal-title":"IEEE Trans. on S.W. Engg"},{"key":"37_CR14","volume-title":"Technical report","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The Temporal Logic of Actions. Technical report, Digital Equipment Corporation (DEC) Systems Research Center, Palo Alto, California, USA, April 1994."},{"key":"37_CR15","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11\u201344, 1995.","journal-title":"Formal Methods in System Design"},{"key":"37_CR16","first-page":"137","volume-title":"Hierarchical correctness proofs for distributed algorithms","author":"N. A. Lynch","year":"1987","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the sixth Annual Symposium on Principles of Distributed Computing, New York, pages 137\u2013151. ACM Press, 1987."},{"key":"37_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993."},{"key":"37_CR18","volume-title":"Technical report","author":"R. Melton","year":"1993","unstructured":"R. Melton, D.L. Dill, and C. Norris Ip. Murphi annotated reference manual, version 2.6. Technical report, Stanford University, Palo Alto, California, USA, November 1993. Written by C. Norris Ip."},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow. Combining model checking and deduction for i\/o-automata. Technical University of Munich. Draft manuscript, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"issue":"2","key":"37_CR20","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"37_CR21","series-title":"Lecture Notes in Computer Science, Volume 939","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification (CAV) 1995, Liege, Belgium, Lecture Notes in Computer Science, Volume 939","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Computer-Aided Verification (CAV) 1995, Liege, Belgium, Lecture Notes in Computer Science, Volume 939, pages 84\u201397. Springer Verlag, July 1995."}],"container-title":["Lecture Notes in Computer Science","FME'96: Industrial Benefit and Advances in Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60973-3_113.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:13Z","timestamp":1605646993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60973-3_113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540609735","9783540497493"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-60973-3_113","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}