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

Professor Mooly (Shmuel) Sagiv, Chair of Software Systems, Fellow of the ACM


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

Research

My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable.

I am interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive process, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic.

I am applying these techniques to verify safety of liveness of distributed systems.

Verifying Liveness and Safety of Distributed Systems

Distributed protocols play a significant role in our daily life. For example, consensus algorithms guarantee the consistency of distributed systems used to control the behavior of autonomous cars, internet of things and smart cities. These systems have severe bugs both in the design and the implementation which have tremendous consequences on our security. Full end-to end formal verification is beyond the reach of existing methods because of the complexity of the protocols and their tricky low-level implementations. Moreover, testing these protocols is ineffective since crucial bugs do occur in rare scenarios.

We plan to develop techniques for semi-automatic formal verification of realistic distributed protocols all the way from the design to the implementation. The idea is to interact with protocol designers in order to harness their understanding of the system without burdening them with the need to understand how formal verification is implemented. The system will solve complicated decidable problems and the user will guide the system towards a proof or bug finding. This is achieved by breaking the verification problem into decidable sub-problems that can be solved using existing mature tools. Our experience to date has been that automated solvers are far more stable when solving problems in decidable logic fragments. Restricting to decidable logics differs from most common approaches to verification, which use undecidable logics. There is a trade-off, however: undecidable logics frequently allow a direct mapping of systems concepts (e.g., arithmetic, quantifiers, data-structures) into the language of the solver, whereas the mapping is not as direct with decidable logic fragments. To address this issue, we keep the user in the loop; in particular, an important step is typically for the user to break the problem into decidable sub-problems using modularity. We have recently built a preliminary prototype tool called Ivy, which can be used to perform automatic reasoning about the designs of simple distributed protocols.

Invariant Checking

We have shown how to perform invariant checking using decidable logic in protocol designs and protocol implementations.

Invariant Inference

We started studying the the decidability of invariant inference.

Quantifier Instantiation

A basic research problem related to invariant checking and invariant inference is given a first order formula, how to instantiate the quantifiers in order to check if a formula is valid. We have recently shown that the bounded horizon technique is rather powerful.

Beyond Safety

Oded Padon's thesis addresses the problem of reasoning about liveness of infinite state systems.

Analyzing Cloud Applications

We plan to develop mechanisms for ensuring the safety of cloud applications. We have developed a system for tracking information flow for cloud applications.

Selected Publications

Recent Papers

Some Talks

Current Grants

Courses (2013-2019)