Abstract

I will talk about the Metarouting project and its implementation in Coq.

Internet routing protocols are build on ideas of classical shortest path algorithms. However, metric and operations on paths in Internet routing are much more complicated. Shortest path algorithms usually require the path algebra to be a semiring in order for the result of the algorithm to make sense. Internet protocols usually fail these conditions.

The aim of Metarouting is to provide a framework for constructing path algebras and inferring properties about them to see if they can be used to find shortest paths. We implement a language (together with its semantics) for specifying path algebras in Coq and prove how constructions of the language propagate properties of interest. Using code extraction we get a formally verified code that computes properties of specified algebras and uses those algebras in shortest path algorithms.

At the end of the talk I will give a little demo.