Abstract
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 SDN architectures make it possible to build rich applications in software, programmers today are forced to deal with numerous low-level details such as encoding high-level policies using low-level hardware primitives, processing asynchronous events, dealing with unexpected failures, etc. This talk will present an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. I will formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. I will describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating the scalability of our tool.
Joint work with Pavol Cerny (TU Wein), Jedidiah McClurg (Colorado School of Mines), and Hossein Hojjat (Tehran).