Mooly Sagiv
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
79
Venues
25
Active years
2005–2024
Best venue rank
A*
Where they publish
- A*PLDI11 papers
- A*CAV10 papers
- AOOPSLA7 papers
- BSAS6 papers
- BVMCAI5 papers
- A*POPL5 papers
- AESOP5 papers
- ATACAS4 papers
- BPPoPP3 papers
- AISSTA3 papers
- BAPLAS3 papers
- BFMCAD2 papers
- AHotOS2 papers
- BLPAR2 papers
- A*OSDI1 paper
- BCLOUD1 paper
- A*AAAI1 paper
- A*IJCAI1 paper
- ASAT1 paper
- AICDT1 paper
- NationalNSDI1 paper
- AICFP1 paper
- ACADE1 paper
- BFOSSACS1 paper
- CSSS1 paper
Papers
79 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2024 | FMCAD | Harnessing SMT Solvers for Reasoning about DeFi Protocols. | Mooly Sagiv |
| 2022 | OSDI | Blockaid: Data Access Policy Enforcement for Web Applications. | Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker |
| 2021 | CAV | Summing up Smart Transitions. | Neta Elad, Sophie Rain, Neil Immerman, Laura Kovcs, Mooly Sagiv |
| 2021 | CLOUD | Cloud-Scale Runtime Verification of Serverless Applications. | Kalev Alpernas, Aurojit Panda, Leonid Ryzhyk, Mooly Sagiv |
| 2019 | CAV | Inferring Inductive Invariants from Phase Structures. | Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv |
| 2019 | HotOS | Synthesizing Cluster Management Code for Distributed Systems. | Lalith Suresh, Joo Loff, Nina Narodytska, Leonid Ryzhyk, Mooly Sagiv, Brian Oki |
| 2019 | PLDI | Simple and precise static analysis of untrusted Linux kernel extensions. | Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv |
| 2018 | AAAI | Verifying Properties of Binarized Deep Neural Networks. | Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh |
| 2018 | FMCAD | Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. | Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham |
| 2018 | IJCAI | Core-Guided Minimal Correction Set and Core Enumeration. | Nina Narodytska, Nikolaj S. Bjrner, Maria-Cristina V. Marinescu, Mooly Sagiv |
| 2018 | PLDI | Modularity for decidability of deductive verification with applications to distributed systems. | Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos |
| 2018 | SAS | Abstract Interpretation of Stateful Networks. | Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner |
| 2018 | SAT | Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. | Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjrner, Mooly Sagiv |
| 2017 | CAV | Verifying Equivalence of Spark Programs. | Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv |
| 2017 | HotOS | Verification in the Age of Microservices. | Aurojit Panda, Mooly Sagiv, Scott Shenker |
| 2017 | ICDT | On the Automated Verification of Web Applications with Embedded SQL. | Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger |
| 2017 | NSDI | Verifying Reachability in Networks with Mutable Datapaths. | Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker |
| 2017 | TACAS | Bounded Quantifier Instantiation for Checking Inductive Invariants. | Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | Property Directed Reachability for Proving Absence of Concurrent Modification Errors. | Asya Frumkin, Yotam M. Y. Feldman, Ondrej Lhotk, Oded Padon, Mooly Sagiv, Sharon Shoham |
| 2017 | VMCAI | Conjunctive Abstract Interpretation Using Paramodulation. | Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv |
| 2016 | PLDI | Ivy: safety verification by interactive generalization. | Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham |
| 2016 | POPL | Decidability of inferring inductive invariants. | Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv |
| 2016 | TACAS | Some Complexity Results for Stateful Network Verification. | Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham |
| 2015 | PLDI | Composing concurrency control. | Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv |
| 2015 | POPL | Decentralizing SDN Policies. | Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham |
| 2015 | PPoPP | Automatic scalable atomicity via semantic locking. | Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav |
| 2015 | SAS | Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. | Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, Hongseok Yang |
| 2014 | CAV | Property-Directed Shape Analysis. | Shachar Itzhaky, Nikolaj S. Bjrner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
| 2014 | ESOP | Checking Linearizability of Encapsulated Extended Operations. | Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv |
| 2014 | ISSTA | Verifying atomicity via data independence. | Ohad Shacham, Eran Yahav, Guy Golan-Gueta, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv, Martin T. Vechev |
| 2014 | PLDI | VeriCon: towards verifying controller programs in software-defined networks. | Thomas Ball, Nikolaj S. Bjrner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky |
| 2014 | POPL | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2014 | PPoPP | Automatic semantic locking. | Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav |
| 2013 | CAV | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | LPAR | Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. | Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |
| 2013 | OOPSLA | Turning nondeterminism into parallelism. | Omer Tripp, Eric Koskinen, Mooly Sagiv |
| 2013 | PLDI | Concurrent libraries with foresight. | Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav |
| 2013 | TACAS | Synthesis of Circular Compositional Program Proofs via Abduction. | Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv |
| 2012 | ESOP | Eventually Consistent Transactions. | Sebastian Burckhardt, Daan Leijen, Manuel Fhndrich, Mooly Sagiv |
| 2012 | ESOP | Reasoning about Lock Placements. | Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv |
| 2012 | OOPSLA | Understanding the behavior of database operations under program control. | Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv |
| 2012 | PLDI | Concurrent data representation synthesis. | Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv |
| 2012 | PLDI | JANUS: exploiting parallelism via hindsight. | Omer Tripp, Roman Manevich, John Field, Mooly Sagiv |
| 2012 | POPL | Abstractions from tests. | Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv |
| 2011 | OOPSLA | Automatic fine-grain locking using shape properties. | Guy Golan-Gueta, Nathan Grasso Bronson, Alex Aiken, G. Ramalingam, Mooly Sagiv, Eran Yahav |
| 2011 | OOPSLA | Testing atomicity of composed concurrent operations. | Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav |
| 2011 | OOPSLA | HAWKEYE: effective discovery of dataflow impediments to parallelization. | Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv |
| 2011 | PLDI | Precise and compact modular procedure summaries for heap manipulating programs. | Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv |
| 2011 | PLDI | Data representation synthesis. | Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv |
| 2010 | APLAS | Data Structure Fusion. | Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv |
| 2010 | ICFP | Specifying and verifying sparse matrix codes. | Gilad Arnold, Johannes Hlzl, Ali Sinan Kksal, Rastislav Bodk, Mooly Sagiv |
| 2010 | OOPSLA | A simple inductive synthesis methodology and its applications. | Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |
| 2010 | OOPSLA | A dynamic evaluation of the precision of static heap abstractions. | Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv |
| 2010 | SAS | Statically Inferring Complex Heap, Array, and Numeric Invariants. | Bill McCloskey, Thomas W. Reps, Mooly Sagiv |
| 2009 | APLAS | Abstract Transformers for Thread Correlation Analysis. | Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv |
| 2009 | CAV | Generalizing DPLL to Richer Logics. | Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv |
| 2009 | POPL | A combination framework for tracking partition sizes. | Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv |
| 2009 | VMCAI | Thread-Modular Shape Analysis. | Mooly Sagiv |
| 2008 | CAV | Proving Conditional Termination. | Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv |
| 2008 | ESOP | Ranking Abstractions. | Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang |
| 2008 | ISSTA | Customization change impact analysis for erp professionals via program slicing. | Nurit Dor, Tal Lev-Ami, Shay Litvak, Mooly Sagiv, Dror Weiss |
| 2008 | SAS | Heap Decomposition for Concurrent Shape Analysis. | Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine |
| 2007 | APLAS | Local Reasoning for Storable Locks and Threads. | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv |
| 2007 | CADE | Labelled Clauses. | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
| 2007 | CAV | Comparison Under Abstraction for Verifying Linearizability. | Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
| 2007 | CAV | Leaping Loops in the Presence of Abstraction. | Thomas Ball, Orna Kupferman, Mooly Sagiv |
| 2007 | CAV | Revamping TVLA: Making Parametric Shape Analysis Competitive. | Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv |
| 2007 | ESOP | Modular Shape Analysis for Dynamically Encapsulated Programs. | Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav |
| 2007 | LPAR | Decidable Fragments of Many-Sorted Logic. | Aharon Abadi, Alexander Moshe Rabinovich, Mooly Sagiv |
| 2007 | PLDI | Thread-modular shape analysis. | Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv |
| 2007 | TACAS | Shape Analysis by Graph Decomposition. | Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv |
| 2007 | VMCAI | Constructing Specialized Shape Analyses for Uniform Change. | Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps |
| 2006 | FOSSACS | A Logic of Reachable Patterns in Linked Data-Structures. | Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani |
| 2006 | ISSTA | Testing, abstraction, theorem proving: better together! | Greta Yorsh, Thomas Ball, Mooly Sagiv |
| 2006 | SAS | Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. | Alexey Loginov, Thomas W. Reps, Mooly Sagiv |
| 2006 | VMCAI | Combining Shape Analyses by Intersecting Abstractions. | Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham |
| 2005 | PPoPP | Scaling model checking of dataraces using dynamic information. | Ohad Shacham, Mooly Sagiv, Assaf Schuster |
| 2005 | SAS | Interprocedural Shape Analysis for Cutpoint-Free Programs. | Noam Rinetzky, Mooly Sagiv, Eran Yahav |
| 2005 | SSS | Self-stabilization Preserving Compiler. | Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv |