Program Synthesis for Network Updates


  Dr. Pavol Cerny, University of Colorado at Boulder

 Program Synthesis for Network Updates


We first give a brief overview of the new field of program synthesis. We describe the role that declarative, logical specifications can play in making programmers more efficient. Second, we describe an application of this approach: synthesis of programs that update network configurations.

Configuration updates are a leading cause of instability in networks. A key factor that makes updates difficult to implement is that networks are distributed systems with hundreds or thousands of nodes all interacting with each other. Even if the initial and final configurations are correct, naively updating individual nodes can easily cause the network to exhibit incorrect behaviors such as forwarding loops, black holes, and security vulnerabilities. This paper presents a new approach to the network update problem: we automatically generate updates that are guaranteed to preserve important correctness properties, given in a temporal logic. Our system is based on counterexample-guided search and incorporates heuristics that quickly identify correct updates in many situations.  We exploit the fact that the search algorithm asks a series of related model checking questions, and develop an efficient incremental LTL model checking algorithm. We present experimental results showing that it efficiently generates updates for real-world topologies with thousands of nodes.

About the presenter
Dr. Pavol Cerny

Affiliation or organization:



Main Seminar Room

Lab/division or program:

Type of event:

Start date and time: 
Tuesday, April 15, 2014 - 10:00am