NV: An Intermediate Language for Network Verification (Nick Ginnarakis, Princeton)

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.