A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol

Timothy Bourke, Rob van Glabbeek, Peter Höfner, Franck Cassez (Editor), Jean-François Raskin (Editor)

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

Abstract / Description of output

The (AODV) routing protocol allows the nodes in a (MANET) or a (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings
EditorsFranck Cassez, Jean-François Raskin
PublisherSpringer, Cham
Pages47-63
Number of pages17
ISBN (Electronic)978-3-319-11936-6
ISBN (Print)978-3-319-11935-9
DOIs
Publication statusPublished - 24 Oct 2014
Event12th International Symposium on Automated Technology for Verification and Analysis, 2014 - sYDNEY, Australia
Duration: 3 Nov 20147 Nov 2014
Conference number: 12

Symposium

Symposium12th International Symposium on Automated Technology for Verification and Analysis, 2014
Abbreviated titleATVA 2014
Country/TerritoryAustralia
CitysYDNEY
Period3/11/147/11/14

Fingerprint

Dive into the research topics of 'A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol'. Together they form a unique fingerprint.

Cite this