Software synthesis is a powerful technique that can dramatically increase the productivity of programmers by automating the construction of complex code. One area where synthesis seems particularly promising is in computer networks. Although Software-Defined Networking (SDN) makes it possible to build rich applications in software, programmers nowadays are forced to deal with numerous low-level details such as encoding high-level policies using low-level hardware primitives, dealing with unexpected failures, debugging a buggy network configurations, etc.
This talk will present highlights from recent work using synthesis to generate correct-by-construction network programs. In the first part of the talk, I will describe an approach for generating configuration updates that are guaranteed to preserve specified invariants. In the second part of the talk, I will present a technique based on Horn clause solving to help network operators fix buggy configurations.
(Joint work with Nate Foster (Cornell University), Pavol Cerny (University of Colorado at Boulder), Jedidiah McClurg (University of Colorado at Boulder), Philipp Ruemmer (Uppsala University))
Hossein Hojjat is an assistant professor in the Computer Science department at the Rochester Institute of Technology (RIT). Before joining RIT, he was a postdoctoral researcher at Cornell University. He earned a PhD in Computer Science from EPFL in 2013. His research interests center on program synthesis and computer-aided verification/synthesis.