CISL Seminar series Presents: Dr. Pavol Cerny, CU, Boulder

Tuesday, April 15, 2014

10:00 AM – 11:00 AM

NCAR Mesa Lab Main Seminar Room

Program Synthesis for Network Updates

 Abstract:

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 you
First name: 
Jennifer
Last name: 
Williamson
Phone extension: 
1224
Announcement contact
First name: 
Jennifer
Last name: 
Williamson
Phone extension: 
1224
Announcement duration
Start: 
Monday, April 14, 2014
End: 
Tuesday, April 15, 2014