[talks] lunchtime Tue Apr 23 talk on automated formal analysis of Internet routing systems

Jennifer Rexford jrex at CS.Princeton.EDU
Wed Apr 17 18:33:49 EDT 2013


Speaker: Anduo Wang, U. Penn, http://www.cis.upenn.edu/~anduo/
Title: Automated Formal Analysis of Internet Routing Systems
Date/time: 12:30-1:20pm Tue Apr 23 (lunch served 12-12:30)
Location: 402 in CS building

Abstract:

The past twenty years have witnessed significant advances in formal
modeling, system verification and testing of network protocols.
However a long-standing challenge in these approaches is the
decoupling of formal reasoning process and the actual distributed
implementation.  This talk presents my thesis work on bridging formal
reasoning and actual implementation in the context of today’s Internet
routing. I will present the Formally Safe Routing (FSR) toolkit, that
combines the use of declarative networking, routing algebra, and SMT
solver techniques, in order to synthesize faithful distributed routing
implementations from verified network models. Next, I will describe
our work on scaling up formal analysis of lnternet-scale
configurations. Our core technique uses a configuration rewriting
calculus for transforming large network configurations into smaller
instances, while preserving routing behaviors. Finally, I conclude
with a discussion of my ongoing and future work, on synthesizing
provably correct network configurations for the emerging Software
Defined Networking (SDN) platforms.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20130417/a533dbf0/attachment.html>


More information about the talks mailing list