BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalizing Metarouting - Vilius Naudziunas
DTSTART:20110215T131500Z
DTEND:20110215T141500Z
UID:TALK29332@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:I will talk about the Metarouting project and its implementati
 on in Coq.\n\nInternet routing protocols are build on ideas of classical s
 hortest path\nalgorithms. However\, metric and operations on paths in Inte
 rnet routing\nare much more complicated. Shortest path algorithms usually 
 require the\npath algebra to be a semiring in order for the result of the 
 algorithm to\nmake sense. Internet protocols usually fail these conditions
 .\n\nThe aim of Metarouting is to provide a framework for constructing pat
 h\nalgebras and inferring properties about them to see if they can be used
 \nto find shortest paths. We implement a language (together with its\nsema
 ntics) for specifying path algebras in Coq and prove how constructions\nof
  the language propagate properties of interest. Using code extraction\nwe 
 get a formally verified code that computes properties of specified\nalgebr
 as and uses those algebras in shortest path algorithms.\n\nAt the end of t
 he talk I will give a little demo.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR