Thu 16 Jun 2016 14:00 - 14:30 at Grand Ballroom San Rafael - Software-Defined Networking Chair(s): Todd Millstein

Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint—one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet’s path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of path-based correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.

Thu 16 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:00: Research Papers - Software-Defined Networking at Grand Ballroom San Rafael
Chair(s): Todd MillsteinUniversity of California, Los Angeles
pldi-2016-papers13:30 - 14:00
Jedidiah McClurgUniversity of Colorado Boulder, Hossein HojjatCornell University, Nate FosterCornell University, Pavol CernyUniversity of Colorado Boulder
Pre-print Media Attached
pldi-2016-papers14:00 - 14:30
Ryan BeckettPrinceton University, Michael GreenbergPomona College, David WalkerPrinceton University
Media Attached
pldi-2016-papers14:30 - 15:00
Ahmed El-HassanyETH Zürich, Jeremie MiserezETH Zürich, Pavol BielikETH Zurich, Switzerland, Laurent VanbeverETH Zürich, Martin VechevETH Zurich
Media Attached