# 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{https://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.