|Time+Place:||Sunday 11/01/2015 14:30 Room 337-8 Taub Bld.|
|Title:||Synthesis and Verification in a Software Defined World|
|Speaker:|| Sharon Shoham Buchbinder - CS-Lecture
|| Affiliation: || School of Computer Science, Academic College of Tel Aviv-Yaffo
|| Host: || Orna Grumberg & Eran Yahav
Software is becoming an integral part of many aspects of our lives. Its correctness is therefore crucial. Correctness of a system is typically defined with respect to a specification. Given such a specification, the classical verification problem is to check whether the system satisfies its specification. However, a more ambitious goal is to construct a provably correct system directly from the specification. The latter problem is called synthesis. The first part of this talk will address the synthesis problem in the context of Software Defined Networking (SDN). SDN is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a ``controller''--- software that operates independently of the network hardware. In practice, having the controller handle events limits the network scalability. Therefore, the feasibility of SDN depends on the ability to efficiently decentralize network event-handling by installing forwarding rules on the switches. However, installing a rule too early or too late may lead to incorrect behavior. In this work we formalize the correctness and optimality requirements for decentralizing network policies. Further, we identify a useful class of network policies which permits automatic synthesis of a controller which performs optimal forwarding rule installation. The second part of the talk will address verification of concurrent programs which are composed of several components. For scaling verification of such programs, compositional verification techniques aim to decompose the verification of the system into the more manageable verification of its components. We present a new compositional model checking technique based on a circular assume-guarantee rule, and provide experimental results comparing it to a well established learning-based non-circular algorithm. The two approaches are comparable on smaller systems, but our technique significantly outperforms the non-circular approach on larger systems. Short Bio: Sharon Shoham received a B.A. degree in Computer Science (summa cum laude) in 2001, a M.Sc. degree (cum laude) in 2004, and a Ph.D. degree in 2009, all from the Computer science department of the Technion-Israel Institute of Technology. She is currently a senior lecturer at the school of Computer Science at the Academic college of Tel Aviv-Yaffo.