Routing information protocol in hol/spin

Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

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


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
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)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000
CountryUnited States

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Routing information protocol in hol/spin'. Together they form a unique fingerprint.

Cite this