Home
Selected Publications
Recent Publications
Some Talks
Research
Students and Visitors
Grants
Courses
Professional Activities
Personal Information

Professor Mooly (Shmuel) Sagiv


School of Computer Science, Tel Aviv University, Email: msagiv at acm dot org, Vitae
Mooly Sagiv

Selected Publications

Recent Papers

Some Talks

Research

My research focuses broadly on easing the task of developing reliable and efficient programs via program analysis. This area combines two disciplines: automated theorem proving and abstract interpretation. In the next 10 years, I am hoping to develop useful techniques in order to change the ways modern software is built addressing the above challenges. These methods will be implemented in real tools and will increase our understanding of the limitations of automatic methods.

I am currently involved in the following three projects.

Analyzing Distributed Systems and Networks

We are aiming to develop techniques for enforcing safety properties of distributed systems including computer networks. Network verification has recently gained popularity in the programming languages and verification community. Much of the recent work in this area has focused on verifying the behavior of simple networks, whose actions are dictated by static, immutable rules configured ahead of time. However, in reality, modern networks contain a variety of middleboxes, whose behavior is affected both by their configuration and by mutable state updated in response to packets received by them Applying formal methods to reason about computer network is a vivid area which

We are also interested in analyzing sophisticated distributed protocols such as Paxos and Raft.

This is a joint project with Katerina Argyraki, Michael Schapira, and Scott Shenker.

Preliminary Results

Analyzing Cloud Applications

The theme of this project is to apply static and dynamic program analysis to improve the utility of cloud programming. Cloud computing is a model for enabling ubiquitous, convenient, on-demand network access to a shared pool of configurable computing resources (e.g., networks, servers, storage, applications, and services) that can be rapidly provisioned and released with minimal management effort or service provider interaction. However, very little tool support, and in particular compile-time tools, are available for helping client programmers produce correct and efficient programs. We are interested in a specific class of cloud applications where distribution is used to scale data processing. In this class, programmers deploy high-level frameworks like Dryad, Hadoop, and Spark to handle low level system issues such as communication, fault tolerance, and scheduling. The code is written using specialized APIs. This drastically simplifies the programming task and allows novice programmers to build interesting distributed client systems. However, a naive program can suffer from huge performance penalties hidden in the interactions between the client code and system's implementation. Moreover, resource-management is a non-trivial task even for expert users due to irregular input data. Indeed, the use of these frameworks is a double-edged sword as it isolates the developer from how her application actually executes. As cloud-based programming becomes main-stream, the lack of tools that can help client programmers verify that their software works as expected becomes a severe disability. Such tools should consider properties such as functional correctness, service availability, reliability, performance and security guarantees. The kind of applications we are interested in are a perfect fit for formal method techniques as they are often written over frameworks that provide most of the generic services required for distributed processing and expose a domain-specific programming model. This leads to rather small programs, however, efficient use of these frameworks is predicated on understanding the intricacies of the programming model and the underlying execution engine.

This is a brand new joint project with Aurojit Panda, Madan Musuvathi, and Noam Rinetzky.

Diagnosable Semi-Automatic Verification

This project derives its motivation from the other projects of analyzing distributed systems and cloud applications. Despite several decades of research, the problem of formal verification of systems with unboundedly many states has resisted effective automation. Our hypothesis is that automated methods are difficult to apply in practice not primarily because they are unreliable, but rather because they are opaque. That is, they fail in ways that are difficult for a human user to understand and to remedy. A practical heuristic method, when it fails, should fail visibly, in the sense that the root cause of the failure is observable to the user. This is in contrast to existing automatic tools which sometimes fail in a non-comprehensible way. We are trying to identify interesting domains in which the verification problem is tractable. We are considering interactive verification. A standard method for proving safety properties of unbounded systems is by finding inductive invariants, i.e., properties which hold in the initial states and are preserved by every step of the execution.

This is a joint project with Nikolaj Bjorner, Neil Immerman, Ken McMillan, and Sharon Shoham

Preliminary Results

More information on current and past research here.

Current Grants

Courses (2013-2016)