Routing information protocol in HOL/SPIN

DOI10.1007/3-540-44659-1_4MaRDI QIDQ2754032zbMATH OpenFDO

Authors Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_4

Mathematics Subject Classification ID

Network protocols (68M12)

Recommendations

• Formal verification of standards for distance vector routing protocols
• The convergency of some routing protocols
• Local model checking and protocol analysis
• A mechanized proof of loop freedom of the (untimed) AODV routing protocol
• A compared study of two correctness proofs for the standardized algorithm of ABR conformance

Cited in

(6)

• Performance analysis and functional verification of the stop-and-wait protocol in HOL
• Developing topology discovery in Event-B
• HOL/SPIN
• Formal verification of standards for distance vector routing protocols
• The convergency of some routing protocols
• Network event recognition

This page was built for publication: Routing information protocol in HOL/SPIN

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754032)