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
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
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
- Vericon: Semi-Automatic Verification of SDN control programs.
We apply Z3 for ensuring the correctness of simple Software Defined (SDN) controller programs.
This is the first work which formally verifies the correctness of controller programs. It also handles parametric topologies.
- Synthesizing provably correct forwarding rules.
We define an optimality criteria for pro-actively installing SDN forwarding rules that guarantee a given forwarding
policy is maintained and show that in certain limited controllers optimal solution can be automatically computed.
- Reasoning about network states.
The use of sophisticated forwarding policies requires software with mutable states.
This is prevalent in NFV, Middleboxes, and Software Defined Networks.
This complicates the task of checking network correctness and induces miss-configuration bugs.
- In SNAPL'15, we show how to verify safety of networks with mutable states using SMT solvers.
- In TACAS'16, we studied the
asymptotic complexity of stateful network verification and consider cases in
which it is feasible to verify safety.
- In VMN, we describe a system for scalable verification of networks using SMT solvers.
- IVY: Interactive Safety Verification via Counterexample Generalization.
In PLDI'16, we present a system called IVY for semi-automatically verifying
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,
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
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
- Effectively Propositional Reasoning about Unbounded Paths
In Itzhaky' Phd thesis, he showed how to harness existing SAT solvers for reasoning in a sound and complete way about
deterministic paths in a dynamically evolving graphs.
Here by deterministic we mean that there exist at one outgoing edge used in the path.
The main idea is to reduce the verification problem to finding the (un)satisafiability of a formula
in Effectively Propositional Logic (EPR).
We believe that these results can be generalized to reason about networks and simple distributed protocols.
These results allows to automatically check the correctness of such systems in a sound and complete way.
However, they rely on providing inductive invariants by the programmer which can be hard in practice.
- Decidability of Inferring Universal Inductive Invariants
In POPL'16, Oded Padon study the decidability of inferring EPR invariants.
This article provides a first step towards understanding when invariants can be inferred.
- Ivy: Interactive Verification of Parameterized Systems via Effectively Propositional Reasoning
The design and implementation of distributed protocols can be very tricky even for experienced researchers.
PLDI'16, we present a system called IVY for semi-automatically verifying distributed protocols.
Ivy is based on the following principles:
- Ivy first attempts to locate counterexamples by bounding the number of protocol actions and
symbolically searching for (unbounded) bad inputs.
- Invariants in Ivy are expressed as universal formulas in relational first-order logic.
Their inductiveness check reduces to unsatisfiability in Effectively Propositional Logic (EPR).
This guarantees that the tool can always decide whether an invariant is inductive or not.
Furthermore, our use of universal formulas guarantees that counterexamples to induction can be presented graphically, allowing
inspection by humans.
- Users can have better insights than the tool by suggesting candidate local invariants,
whose conjunction comprises a global inductive invariant.
More information on current and past research here.
- 2013-18 Verifying and Synthesizing Software Compositions, ERC advanced grant
We are looking for outstanding students with a solid background in programming languages, formal methods, and algorithms.
Positions are available for PhD and postdoctoral studies. Only top students
will be considered.
- 2011-15 Enabling Software Scalability via Dynamic and Static Program Analysis Israel Science Foundation