{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:58:11Z","timestamp":1742403491585},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_4","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"53-72","source":"Crossref","is-referenced-by-count":3,"title":["Routing Information Protocol in HOL\/SPIN"],"prefix":"10.1007","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[]},{"given":"Carl A.","family":"Gunter","sequence":"additional","affiliation":[]},{"given":"Davor","family":"Obradovic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Dimitri P. Bertsekas and Robert Gallager. Data Networks. Prentice Hall, 1991."},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"Edmund M. Clarke and Jeannette M. Wing. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4):626\u2013643, December 1996. report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research.","journal-title":"ACM Computing Surveys"},{"key":"4_CR3","unstructured":"D. Cypher, D. Lee, M. Martin-Villalba, C. Prins, and D. Su. Formal Specification, Verification, and Automatic Test Generation of ATM Routing Protocol: PNNI. In Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE\/PSTV) IFIP, November 1998."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"J.J. Garcia-Luna-Aceves and Shree Murthy. A Loop-Free Path-Finding Algorithm: Specification, Verification and Complexity. In Proceedings of IEEE INFOCOM\u2019 95, April 1995.","DOI":"10.21236\/ADA461943"},{"key":"4_CR5","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Timothy G. Griffin and Gordon Wilfong. An analysis of BGP convergence properties. In Guru Parulkar and Jonathan S. Turner, editors, Proceedings of ACM SIGCOMM\u2019 99 Conference, pages 277\u2013288, Boston, August 1999.","DOI":"10.1145\/316194.316231"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Ahmed Helmy, Deborah Estrin, and Sandep Gupta. Fault-oriented Test Generation for Multicast Routing Protocol Design. In Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE\/PSTV) IFIP, November 1998.","DOI":"10.1007\/978-0-387-35394-4_6"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"C. Hendrick. Routing information protocol. RFC 1058, IETF, June 1988.","DOI":"10.17487\/rfc1058"},{"key":"4_CR9","unstructured":"Home page for the HOL interactive theorem proving system, http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL ."},{"key":"4_CR10","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"4_CR11","unstructured":"Christian Huitema. Routing in the Internet. Prentice Hall, 1995."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"G. Malkin. RIP Version 2 Carrying Additional Information. IETF RFC 1388, January 1993.","DOI":"10.17487\/rfc1388"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1023\/A:1008729625855","volume":"16","author":"A. Mokkedem","year":"2000","unstructured":"Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones, and Ganesh Gopalakrishnan. Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. Formal Methods in System Design, 16(1):93\u2013119, January 2000.","journal-title":"Formal Methods in System Design"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Olaf M\u00fcller and Tobias Nipkow. Combining model checking and deduction for i\/o-automata. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, May 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Shree Murthy and J.J. Garcia-Luna-Aceves. An efficient routing protocol for wireless networks. ACM Mobile Netowrks and Applications Journal, October 1996. Special Issue on Routing in Mobile Communication Networks.","DOI":"10.1007\/BF01193336"},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0031813","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u2019 96)","author":"N. Shankar","year":"1996","unstructured":"N. Shankar. PVS: Combining specification, proof checking, and model checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 96), volume 1166 of Lecture Notes in Computer Science, pages 257\u2013264, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"4_CR17","unstructured":"Home page for the SPIN model checker. http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html ."},{"key":"4_CR18","unstructured":"Bow-Yaw Wang, Jos\u00e9 Meseguer, and Carl A. Gunter. Specification and formal verification of a PLAN algorithm in Maude. In Proceedings of the International workshop on Distributed System Valdiation and Verification, pages E:49\u2013E:56. IEEE Computer Society Press, April 2000."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:33:00Z","timestamp":1556695980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}