Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Routing


view this post on Zulip Email Gateway (Aug 22 2022 at 13:53):

From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry, on Routing, by Julius Michaelis and Cornelius Diekmann:

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.

Full details here: https://www.isa-afp.org/entries/Routing.shtml

Larry Paulson


Last updated: Nov 21 2024 at 12:39 UTC