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 http://www2.mta.ac.il/~sharon.shoham/
Affiliation: School of Computer Science, Academic College of Tel Aviv-Yaffo
Host: Orna Grumberg & Eran Yahav

Abstract:


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.