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.
  author  = {Julius Michaelis and Cornelius Diekmann},
  title   = {Routing},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2016,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: IP_Addresses, Simple_Firewall
Used by: Iptables_Semantics, LOFT