@inproceedings{5736dc2897a54f3d9325ec7691ef4de2,
title = "A mechanized proof of loop freedom of the (untimed) AODV routing protocol",
abstract = "The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is {\textquoteleft}loop free{\textquoteright} 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.",
author = "Timothy Bourke and \{van Glabbeek\}, Rob and Peter H{\"o}fner and \{van Glabbeek\}, Rob",
note = "Publisher Copyright: {\textcopyright} 2014 Springer International Publishing Switzerland.; 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 ; Conference date: 03-11-2014 Through 07-11-2014",
year = "2014",
month = jan,
day = "1",
doi = "10.1007/978-3-319-11936-6\_5",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "47--63",
editor = "Franck Cassez and Jean-Fran{\c c}ois Raskin",
booktitle = "Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings",
}