NV: An Intermediate Language for Network Verification (Nick Ginnarakis, Princeton)
Tuesday, March 3, 2020
CS 3310, Computer Sciences
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.