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

Timothy Bourke, Rob J. van Glabbeek, Peter Hfner

Browse the full ATVA paper archive.