Mooly Sagiv

ORCID

Publication Activity (10 Years)

Years Active: 2005-2023
Publications (10 Years): 60

Top Venues

CoRR

Proc. ACM Program. Lang.

PLDI

POPL

Publications

Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, Mooly Sagiv
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. IEEE Trans. Dependable Secur. Comput. 20 (3) (2023)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Property-directed reachability as abstract interpretation in the monotone theory. Proc. ACM Program. Lang. 6 (POPL) (2022)
Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker
Blockaid: Data Access Policy Enforcement for Web Applications. CoRR (2022)
Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker
Blockaid: Data Access Policy Enforcement for Web Applications. OSDI (2022)
Kalev Alpernas, Aurojit Panda, Mooly Sagiv
This is not the End: Rethinking Serverless Function Termination. CoRR (2022)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR (2021)
Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
Summing Up Smart Transitions. CoRR (2021)
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Some Complexity Results for Stateful Network Verification. CoRR (2021)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Learning the boundary of inductive invariants. Proc. ACM Program. Lang. 5 (POPL) (2021)
Uri Kirstein, Shelly Grossman, Michael Mirkin, James Wilcox, Ittay Eyal, Mooly Sagiv
Phoenix: A Formally Verified Regenerating Vault. CoRR (2021)
Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv
Summing up Smart Transitions. CAV (1) (2021)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR (2021)
Kalev Alpernas, Aurojit Panda, Leonid Ryzhyk, Mooly Sagiv
Cloud-Scale Runtime Verification of Serverless Applications. SoCC (2021)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57 (2) (2021)
Mooly Sagiv
Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs. SMT (2020)
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv
Taming callbacks for smart contract modularity. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
Complexity and information in invariant inference. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox
Learning the Boundary of Inductive Invariants. CoRR (2020)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. Log. Methods Comput. Sci. 15 (3) (2019)
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham
Complexity and Information in Invariant Inference. CoRR (2019)
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
Inferring Inductive Invariants from Phase Structures. CoRR (2019)
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Some complexity results for stateful network verification. Formal Methods Syst. Des. 54 (2) (2019)
Lalith Suresh, João Loff, Nina Narodytska, Leonid Ryzhyk, Mooly Sagiv, Brian Oki
Synthesizing Cluster Management Code for Distributed Systems. HotOS (2019)
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI (2019)
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv
Inferring Inductive Invariants from Phase Structures. CAV (2) (2019)
Lalith Suresh, João Loff, Faria Kalim, Nina Narodytska, Leonid Ryzhyk, Sahan Gamage, Brian Oki, Zeeshan Lokhandwala, Mukesh Hira, Mooly Sagiv
Automating Cluster Management with Weave. CoRR (2019)
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjørner, Mooly Sagiv
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. CoRR (2018)
Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein
Secure serverless computing using dynamic information flow control. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj Bjørner, Mooly Sagiv
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT (2018)
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. Proc. ACM Program. Lang. 2 (POPL) (2018)
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. FMCAD (2018)
Nina Narodytska, Nikolaj Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
Core-Guided Minimal Correction Set and Core Enumeration. IJCAI (2018)
Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein
Secure Serverless Computing Using Dynamic Information Flow Control. CoRR (2018)
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. CoRR (2018)
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos
Modularity for decidability of deductive verification with applications to distributed systems. PLDI (2018)
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Abstract Interpretation of Stateful Networks. SAS (2018)
Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
Verifying Properties of Binarized Deep Neural Networks. AAAI (2018)
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2 (POPL) (2018)
Aurojit Panda, Mooly Sagiv, Scott Shenker
Verification in the Age of Microservices. HotOS (2017)
Nikolaj Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv
Abduction for Learning Smart City Rules. GCAI (2017)
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Paxos Made EPR: Decidable Reasoning about Distributed Protocols. CoRR (2017)
Isil Dillig, Thomas Dillig, Boyang Li, Kenneth L. McMillan, Mooly Sagiv
Synthesis of circular compositional program proofs via abduction. Int. J. Softw. Tools Technol. Transf. 19 (5) (2017)
Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
Verifying Properties of Binarized Deep Neural Networks. CoRR (2017)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Reachability in Networks with Mutable Datapaths. NSDI (2017)
Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner
Modular Safety Verification for Stateful Networks. CoRR (2017)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. TACAS (1) (2017)
Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv
Verifying Equivalence of Spark Programs. CAV (2) (2017)
Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
Automatic Scalable Atomicity via Semantic Locking. ACM Trans. Parallel Comput. 3 (4) (2017)
Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham
Property Directed Reachability for Proving Absence of Concurrent Modification Errors. VMCAI (2017)
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
Bounded Quantifier Instantiation for Checking Inductive Invariants. CoRR (2017)
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv
Conjunctive Abstract Interpretation Using Paramodulation. VMCAI (2017)
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
On the Automated Verification of Web Applications with Embedded SQL. ICDT (2017)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Reachability in Networks with Mutable Datapaths. CoRR (2016)
Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv
Decidability of inferring inductive invariants. POPL (2016)
Mooly Sagiv
Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). FSTTCS (2016)
Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger
On the automated verification of web applications with embedded SQL. CoRR (2016)
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
Ivy: safety verification by interactive generalization. PLDI (2016)
Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham
Some Complexity Results for Stateful Network Verification. TACAS (2016)
Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
Automatic scalable atomicity via semantic locking. PPOPP (2015)
Aurojit Panda, Katerina J. Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker
New Directions for Network Verification. SNAPL (2015)
Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv
Composing concurrency control. PLDI (2015)
Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham
Decentralizing SDN Policies. POPL (2015)
Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, Hongseok Yang
Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. SAS (2015)
Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
Automatic semantic locking. PPOPP (2014)
Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur
Property-Directed Shape Analysis. CAV (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
Modular reasoning about heap paths via effectively propositional formulas. POPL (2014)
Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky
VeriCon: towards verifying controller programs in software-defined networks. PLDI (2014)
Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv
Checking Linearizability of Encapsulated Extended Operations. ESOP (2014)
Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker
Verifying Isolation Properties in the Presence of Middleboxes. CoRR (2014)
Ohad Shacham, Eran Yahav, Guy Golan-Gueta, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv, Martin T. Vechev
Verifying atomicity via data independence. ISSTA (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV (2013)
Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv
Synthesis of Circular Compositional Program Proofs via Abduction. TACAS (2013)
Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler
Principles of POPL. ACM SIGPLAN Notices 48 (4S) (2013)
Jörg Kreiker, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav
Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs. Programming Logics (2013)
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. LPAR (2013)
Omer Tripp, Eric Koskinen, Mooly Sagiv
Turning nondeterminism into parallelism. OOPSLA (2013)
Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav
Concurrent libraries with foresight. PLDI (2013)
Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv
Abstractions from tests. POPL (2012)
Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher
An introduction to data representation synthesis. Commun. ACM 55 (12) (2012)
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
Concurrent data representation synthesis. PLDI (2012)
Omer Tripp, Roman Manevich, John Field, Mooly Sagiv
JANUS: exploiting parallelism via hindsight. PLDI (2012)
Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv
Understanding the behavior of database operations under program control. OOPSLA (2012)
Mooly Sagiv
POPL'11 program chair's report. ACM SIGPLAN Notices 47 (4a) (2012)
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
Reasoning about Lock Placements. ESOP (2012)
Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, Mooly Sagiv
Eventually Consistent Transactions. ESOP (2012)
Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv
HAWKEYE: effective discovery of dataflow impediments to parallelization. OOPSLA (2011)
Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv
Precise and compact modular procedure summaries for heap manipulating programs. PLDI (2011)
Guy Golan-Gueta, Nathan Grasso Bronson, Alex Aiken, G. Ramalingam, Mooly Sagiv, Eran Yahav
Automatic fine-grain locking using shape properties. OOPSLA (2011)
Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav
Testing atomicity of composed concurrent operations. OOPSLA (2011)
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
Data representation synthesis. PLDI (2011)
Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv
A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. 32 (2) (2010)
Bill McCloskey, Thomas W. Reps, Mooly Sagiv
Statically Inferring Complex Heap, Array, and Numeric Invariants. SAS (2010)
Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv
A dynamic evaluation of the precision of static heap abstractions. OOPSLA (2010)
Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv
Specifying and verifying sparse matrix codes. ICFP (2010)
Eran Yahav, Mooly Sagiv
Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32 (5) (2010)
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
Data Structure Fusion. APLAS (2010)
Aharon Abadi, Alexander Rabinovich, Mooly Sagiv
Decidable fragments of many-sorted logic. J. Symb. Comput. 45 (2) (2010)
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
A simple inductive synthesis methodology and its applications. OOPSLA (2010)

Mooly Sagiv.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Mooly Sagiv