Nick Giannarakis (Dave Walker student at Princeton) is visiting us Monday to Wed nextÂweek.
He will give the following talk on Tuesday at 1pm in 3310
Title: NV: An Intermediate Language for Network Verification
Abstract:
In recent years network misconfiguration-induced outages have become rampantÂboth in frequency and impact. 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 routing 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 (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. Lastly, I will briefly discuss future directions for NV, such asÂmodelingÂthe data plane and extensions to the language to support this.
Bio:ÂNick Giannarakis is a 5th year PhD student at Princeton University, working with Professor David Walker. His research interests revolve around the design and implementation of programming languages, and he enjoys applying techniques from PL to help people build practical and correct systems. Before coming to Princeton he obtained a masterâs degree in Computer Science from Ãcole Normale SupÃrieure Paris-Saclay, and prior to that he completed his undergraduate degree in Electrical and Computer Engineering at the National Technical University of Athens.Â
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}