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 proofautomation by:
(i) exploring modularity of the system
and
(ii) relying on semiautomatic and interactive process, where the user manually and interactively guides the proof
automation, and (iii) simplifying the verification task by using domainspecific 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 endto end formal verification is beyond the reach of existing
methods because of the complexity of the protocols and their tricky lowlevel implementations. Moreover,
testing these protocols is ineffective since crucial bugs do occur in rare scenarios.
We plan to develop techniques for semiautomatic 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 subproblems 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 tradeoff, however: undecidable logics
frequently allow a direct mapping of systems concepts (e.g., arithmetic, quantifiers, datastructures) 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 subproblems 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.
 Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh:
Verifying Properties of Binarized Deep Neural Networks. AAAI 2018: 66156624
 Temporal Prophecy for Proving Temporal Properties of InfiniteState 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:1118: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 GolanGueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar:
Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2(POPL): 48:148:28 (2018)
 Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Reducing liveness to safety in firstorder logic. PACMPL 2(POPL): 26:126: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.
 EffectivelyPropositional Reasoning about Reachability in Linked Data Structures..
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv: CAV 2013: 756772

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 ObjectOriented Programming, Systems, Languages, and Applications 2011.
 Eran Yahav, Mooly Sagiv
Verifying safety properties of concurrent heapmanipulating 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 firstorder logic with applications to verification of linked data structures
Tal LevAmi, 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 LevAmi, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine: SAS 2008: 363377
 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 SIGPLANSIGACT 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
3Valued Logic. Mooly Sagiv, Thomas Reps, and Reinhard
Wilhelm. Journal ACM Transactions on Programming Languages and
Systems (TOPLAS) Volume 24 Issue 3, May 2002
 Precise
interprocedural dataflow analysis via graph reachability
Reps, T., Horwitz, S., and Sagiv, M.,
the TwentySecond ACM Symposium on Principles of Programming Languages, (San Francisco, CA, Jan. 2325, 1995), pp. 4960
 Precise interprocedural dataflow analysis with applications to constant propagation
Sagiv, M., Reps, T., and Horwitz, S., . Theoretical Computer Science 167 (1996), 131170
 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.)
