Nick Giannarakis will present his Pre FPO "An Intermediate Language for Network Verification" on Friday, February 14, 2020 at 2pm in CS 302. The members of his committee are as follows: David Walker (adviser), Aarti Gupta (reader), Ratul Mahajan (UW, reader), Andrew Appel and Jennifer Rexford (examiners). Everyone is invited to attend his talk. The talk title and abstract follow below. Title: An Intermediate Language for Network Verification Abstract: In recent years network misconfiguration-induced outages have become rampant both in frequency and impact. Misconfigurations often occur in the control plane, a distributed system responsible for exchanging routing information among routers. To configure routing policies, operators have to issue per-device configurations in low-level languages, while accounting for interactions with external networks, as well as potential device or link failures. For large networks --- which may involve millions of lines of configuration spread across thousands of devices --- this is a challenging task. To aid operators, researchers have developed a range of static analysis tools to establish correctness properties of network control planes. However, developing and maintaining such tools is an enormous undertaking because of the complexity of configuration languages and the plethora of features the protocols pack. Inspired by prior work on intermediate languages for verification such as Boogie and Why3, I will describe the design and implementation of NV, an intermediate language for verification of routing protocols and their configurations. NV was designed to strike a balance between expressiveness, tractability and ease of use. I will explain how to leverage NV's design to develop efficient implementations (often outperforming the current state-of-the-art by an order of magnitude) of network analyses such as simulation and SMT-based verification. Beyond these standard techniques, NV also facilitates the rapid development of new analyses; I will describe the key insights behind a highly scalable fault tolerance analysis, and present its implementation in the NV language. Finally, I will present a new approach to network compression, implemented on top of NV, and suitable for reasoning about fault-tolerance properties.