Formalizing Metarouting

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

• Vilius Naudziunas
• Tuesday 15 February 2011, 13:15-14:15
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.