<html><body><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div data-marker="__QUOTED_TEXT__"><div class=""><div><blockquote class=""><div class=""><div class=""><div style="font-family: garamond, 'new york', times, serif; font-size: 12pt;" class="" data-mce-style="font-family: garamond, 'new york', times, serif; font-size: 12pt;"><div class=""><div class="" style="word-wrap: break-word;" data-mce-style="word-wrap: break-word;"><div class="">Ryan Beckett will present his Pre-FPO on Tuesday, November 14, 2017 at 11:30am in CS 233.<br class="">
</div><div class=""><br></div><div class="">The members of his committee are as follows:</div><div class=""><b class="">Advisor:</b> David Walker<br></div>
<div class=""><b class="">Readers:</b> Aarti Gupta, Ratul Mahajan (Microsoft)</div>
<div class=""><b class="">Non-Readers:</b> Jennifer Rexford, Nick Feamster</div>
<div class=""><br class="">
</div><div class="">Everyone is invited to attend his talk. The talk title and abstract follow below</div><div class=""><br data-mce-bogus="1"></div>
<div class=""><b class="">Title:</b></div>
<div class="">Network Control Plane Verification and Synthesis</div>
<div class=""><br class="">
</div>
<div class=""><b class="">Abstract:</b></div>
<div class="">
<div class="">Network control planes for traditional networks are highly complex distributed systems. Network devices use multiple protocols to exchange routing information about available paths to a destination, and how they process this information depends
on their local configuration files. Each configuration file often consists of thousands of lines of assembly-like directives -- making it hard for humans to reason about individual device behaviors and even harder to reason about the network behavior that
emerges through the distributed interactions of all devices. Consequently, network misconfiguration caused by human error remains a leading cause of network downtime. In my thesis, I develop novel approaches to automatically verify and synthesize network device
configurations in a scalable manner from high-level specifications about their correctness.</div>
<div class=""><br class="">
</div>
<div class="">In the first part of this talk, I will describe a general approach to network control plane verification based on translating unmodified network configurations into logical formulae that capture both the stable states to which the network protocols
converge as well as their impact on packet forwarding. Using an off-the-shelf Satisfiability Modulo Thoery (SMT) solver, we can verify adherence to a wide range of properties including reachability, fault-tolerance, router equivalence, and load balancing,
for all possible outcomes of the control plane. In the second part of my talk, I will describe a new high-level network routing language and associated compilation techniques to generate device configurations that are correct-by-construction. Throughout both
parts of the talk, I will describe the role of network abstraction in making these approaches scale to large, modern networks.</div>
</div>
<div class=""><br></div></div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
<br class="">
</div><br></div></div></body></html>