Routing

Title:	Routing
Authors:	Julius Michaelis and Cornelius Diekmann
Submission date:	2016-08-31
Abstract:	This entry contains definitions for routing with routing tables/longest prefix matching. A routing table entry is modelled as a record of a prefix match, a metric, an output port, and an optional next hop. A routing table is a list of entries, sorted by prefix length and metric. Additionally, a parser and serializer for the output of the ip-route command, a function to create a relation from output port to corresponding destination IP space, and a model of a Linux-style router are included.
BibTeX:	@article{Routing-AFP, author = {Julius Michaelis and Cornelius Diekmann}, title = {Routing}, journal = {Archive of Formal Proofs}, month = aug, year = 2016, note = {\url{http://isa-afp.org/entries/Routing.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Simple_Firewall
Used by:	Iptables_Semantics
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.