<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><span style="font-family: arial, sans-serif; font-size: 13px; ">Speaker: Anduo Wang, U. Penn, </span><a href="http://www.cis.upenn.edu/~anduo/">http://www.cis.upenn.edu/~anduo/</a></div><div><span style="font-family: arial, sans-serif; font-size: 13px; ">Title: </span><span style="font-family: arial, sans-serif; font-size: 13px; ">Automated Formal Analysis of Internet Routing Systems</span></div><div><span style="font-family: arial, sans-serif; font-size: 13px; ">Date/time: 12:30-1:20pm Tue Apr 23 (lunch served 12-12:30)</span></div><div><font face="arial, sans-serif"><span style="font-size: 13px;">Location: 402 in CS building</span></font></div><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">Abstract:</span><div><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">The past twenty years have witnessed significant advances in formal</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">modeling, system verification and testing of network protocols.</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">However a long-standing challenge in these approaches is the</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">decoupling of formal reasoning process and the actual distributed</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">implementation. This talk presents my thesis work on bridging formal</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">reasoning and actual implementation in the context of today’s Internet</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">routing. I will present the Formally Safe Routing (FSR) toolkit, that</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">combines the use of declarative networking, routing algebra, and SMT</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">solver techniques, in order to synthesize faithful distributed routing</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">implementations from verified network models. Next, I will describe</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">our work on scaling up formal analysis of lnternet-scale</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">configurations. Our core technique uses a configuration rewriting</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">calculus for transforming large network configurations into smaller</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">instances, while preserving routing behaviors. Finally, I conclude</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">with a discussion of my ongoing and future work, on synthesizing</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">provably correct network configurations for the emerging Software</span><br style="font-family: arial, sans-serif; font-size: 13px; "><span style="font-family: arial, sans-serif; font-size: 13px; ">Defined Networking (SDN) platforms.</span></div></body></html>