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
(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
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.
We have shown how to perform invariant checking using decidable logic in
protocol designs and
We started studying the
the decidability of invariant inference.
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.
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.
- Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh:
Verifying Properties of Binarized Deep Neural Networks. AAAI 2018: 6615-6624
- Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelsk, Mooly Sagiv, Sharon Shoham. FMCAD 2018.
- Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein:
Secure serverless computing using dynamic information flow control. PACMPL 2(OOPSLA): 118:1-118:26 (2018)
- Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
Marcelo Taube, Giuliano Losa, Kenneth McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos.
- Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar:
Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2(POPL): 48:1-48:28 (2018)
- Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Reducing liveness to safety in first-order logic. PACMPL 2(POPL): 26:1-26:33 (2018)
- Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017.
- Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham. TACAS 2017.
- Conjunctive Abstract Interpretation using Paramodulation
Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv. VMCAI 2017
- IVY: Interactive Safety Verification via Counterexample Generalization
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhotak, Oded Padon, Mooly Sagiv, Sharon Shoham. VMCAI 2017.
Oded Padon, Kenneth McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham. PLDI 2016.
- Decidability of Inferring Inductive Invariants
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv. POPL 2016
- New Directions for Network Verification
Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker
- Decentralizing SDN Policies
Oded Padon, Neil Immerman, Ori Lahav, Aleksandr Karbyshev, Mooly Sagiv, Sharon Shoham. POPL 2015.
- Effectively-Propositional Reasoning about Reachability in Linked Data Structures..
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv: CAV 2013: 756--772
An Introduction to Data Representation Synthesis.
- Testing Atomicity of Composed Concurrent Operations.
O. Shacham, N. Bronson, A. Aiken, M. Sagiv, M. Vechev, and E. Yahav. Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages, and Applications 2011.
- Eran Yahav, Mooly Sagiv
Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5): (2010)
- Finite differencing of logical formulas for static analysis.
Thomas W. Reps, Mooly Sagiv, Alexey Loginov: ACM Trans. Program. Lang. Syst. 32(6): (2010)
- Simulating reachability using first-order logic with applications to verification of linked data structures
Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Mooly Sagiv, Siddharth Srivastava, Greta Yorsh.
Logical Methods in Computer Science 5(2): (2009)
- Heap Decomposition for Concurrent Shape Analysis
Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine: SAS 2008: 363-377
- A semantics for procedure local heaps and its abstractions,
N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm.
POPL '05: 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, 2005
- CSSV: Towards a
Realistic Tool for Statically Detecting All Buffer Overflows in
C Nurit Dor, Michael Rodeh, and Mooly Sagiv. PLDI 2003
- Parametric Shape Analysis via
3-Valued Logic. Mooly Sagiv, Thomas Reps, and Reinhard
Wilhelm. Journal ACM Transactions on Programming Languages and
Systems (TOPLAS) Volume 24 Issue 3, May 2002
interprocedural dataflow analysis via graph reachability
Reps, T., Horwitz, S., and Sagiv, M.,
the Twenty-Second ACM Symposium on Principles of Programming Languages, (San Francisco, CA, Jan. 23-25, 1995), pp. 49-60
- Precise interprocedural dataflow analysis with applications to constant propagation
Sagiv, M., Reps, T., and Horwitz, S., . Theoretical Computer Science 167 (1996), 131-170
- Speeding up slicing.
T. Reps, S. Horwitz, M. Sagiv, M., and G. Rosay. In SIGSOFT '94:
Proceedings of the Second ACM SIGSOFT Symposium on the Foundations
of Software Engineering (Awarded an ACM SIGSOFT Retrospective
Impact Paper Award 2011.)