Routing information protocol in hol/spin

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We provide a proof using HOL and SPIN of convergence for the Routing Information Protocol (RIP), an internet protocol based on distance vector routing. We also calculate a sharp realtime bound for this convergence. This extends existing results to deal with the RIP standard itself, which has complexities not accounted for in theorems about abstract versions of the protocol. Our work also provides a case study in the combined use of a higher-order theorem prover and a model checker. The former is used to express abstraction properties and inductions, and structure the high-level proof, while the latter deals efficiently with case analysis of finitary properties.

Original languageEnglish (US)
Title of host publicationTheorem Proving in Higher Order Logics - 13th International Conference, TPHOLs 2000, Proceedings
EditorsMark Aagaard, John Harrison
PublisherSpringer-Verlag
Pages53-72
Number of pages20
ISBN (Print)9783540678632
StatePublished - Jan 1 2000
Externally publishedYes
Event13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000 - Portland, United States
Duration: Aug 14 2000Aug 18 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1869
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000
CountryUnited States
CityPortland
Period8/14/008/18/00

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Bhargavan, K., Gunter, C. A., & Obradovic, D. (2000). Routing information protocol in hol/spin. In M. Aagaard, & J. Harrison (Eds.), Theorem Proving in Higher Order Logics - 13th International Conference, TPHOLs 2000, Proceedings (pp. 53-72). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1869). Springer-Verlag.