|
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.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
IP_Addresses, Simple_Firewall |
Used by: |
Iptables_Semantics, LOFT |
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.
|
|