University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Formalizing Metarouting

Formalizing Metarouting

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact William Denman.

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.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity