Networks interconnect the digital world and provide numerous services we all depend upon. Due to ever-growing complexity in network sizes and design features, it is important but challenging to ensure their correct operation. In this talk, I will describe two recent efforts where we use network abstractions to improve methods for formal reasoning about network behavior. In the first, I will focus on modular reasoning about network routing, where a user annotates each router by an abstract interface and our tool automatically checks that these interfaces are inductive and correct. In the second, we use an abstraction over input packet queues on a switch, and combine it with a reduction to answer queries related to network switch performance. In both methods, the abstractions are sound and provide improvements by orders of magnitude in comparison to baseline approaches.

This talk describes joint work with Dexin Zhang, Divya Raghunathan, Maria Apostolaki and David Walker.