default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDShmuel Sagiv
Mooly Sagiv
Person information
- affiliation: Tel Aviv University, Israel
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j41]Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, Chandrakana Nandi:
Practical Verification of Smart Contracts using Memory Splitting. Proc. ACM Program. Lang. 8(OOPSLA2): 2402-2433 (2024)- 2023
- [j40]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): 1878-1904 (2023) - [j39]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): 2256-2273 (2023) - 2022
- [j38]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): 1-31 (2022) - [c141]Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker:
Blockaid: Data Access Policy Enforcement for Web Applications. OSDI 2022: 701-718 - [i25]Wen Zhang, Eric Sheng, Michael Alan Chang, Aurojit Panda, Mooly Sagiv, Scott Shenker:
Blockaid: Data Access Policy Enforcement for Web Applications. CoRR abs/2205.06911 (2022) - [i24]Kalev Alpernas, Aurojit Panda, Mooly Sagiv:
This is not the End: Rethinking Serverless Function Termination. CoRR abs/2211.02330 (2022) - 2021
- [j37]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): 246-269 (2021) - [j36]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Learning the boundary of inductive invariants. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [c140]Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv:
Summing up Smart Transitions. CAV (1) 2021: 317-340 - [c139]Kalev Alpernas, Aurojit Panda, Leonid Ryzhyk, Mooly Sagiv:
Cloud-Scale Runtime Verification of Serverless Applications. SoCC 2021: 92-107 - [i23]Neta Elad, Sophie Rain, Neil Immerman, Laura Kovács, Mooly Sagiv:
Summing Up Smart Transitions. CoRR abs/2105.07663 (2021) - [i22]Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems. CoRR abs/2106.00966 (2021) - [i21]Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Some Complexity Results for Stateful Network Verification. CoRR abs/2106.01030 (2021) - [i20]Uri Kirstein, Shelly Grossman, Michael Mirkin, James Wilcox, Ittay Eyal, Mooly Sagiv:
Phoenix: A Formally Verified Regenerating Vault. CoRR abs/2106.01240 (2021) - [i19]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. CoRR abs/2111.00324 (2021) - 2020
- [j35]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): 209:1-209:30 (2020) - [j34]Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Complexity and information in invariant inference. Proc. ACM Program. Lang. 4(POPL): 5:1-5:29 (2020) - [c138]Mooly Sagiv:
Invited Talk: Harnessing SMT Solvers for Verifying Low Level Programs. SMT 2020: 2 - [i18]Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Learning the Boundary of Inductive Invariants. CoRR abs/2008.09909 (2020)
2010 – 2019
- 2019
- [j33]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): 191-231 (2019) - [j32]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) - [c137]Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv:
Inferring Inductive Invariants from Phase Structures. CAV (2) 2019: 405-425 - [c136]Lalith Suresh, João Loff, Nina Narodytska, Leonid Ryzhyk, Mooly Sagiv, Brian Oki:
Synthesizing Cluster Management Code for Distributed Systems. HotOS 2019: 45-50 - [c135]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: 1069-1084 - [i17]Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv:
Inferring Inductive Invariants from Phase Structures. CoRR abs/1905.07739 (2019) - [i16]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 abs/1909.03130 (2019) - [i15]Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Complexity and Information in Invariant Inference. CoRR abs/1910.12256 (2019) - 2018
- [j31]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): 118:1-118:26 (2018) - [j30]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): 26:1-26:33 (2018) - [j29]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): 48:1-48:28 (2018) - [c134]Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh:
Verifying Properties of Binarized Deep Neural Networks. AAAI 2018: 6615-6624 - [c133]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: 1-11 - [c132]Nina Narodytska, Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv:
Core-Guided Minimal Correction Set and Core Enumeration. IJCAI 2018: 1353-1361 - [c131]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: 662-677 - [c130]Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Abstract Interpretation of Stateful Networks. SAS 2018: 86-106 - [c129]Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv:
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. SAT 2018: 438-449 - [i14]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 abs/1801.04032 (2018) - [i13]Svyatoslav Korneev, Nina Narodytska, Luca Pulina, Armando Tacchella, Nikolaj S. Bjørner, Mooly Sagiv:
Constrained Image Generation Using Binarized Neural Networks with Decision Procedures. CoRR abs/1802.08795 (2018) - [i12]Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein:
Secure Serverless Computing Using Dynamic Information Flow Control. CoRR abs/1802.08984 (2018) - 2017
- [j28]Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham:
Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA): 108:1-108:31 (2017) - [j27]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): 535-547 (2017) - [j26]Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav:
Automatic Scalable Atomicity via Semantic Locking. ACM Trans. Parallel Comput. 3(4): 21:1-21:29 (2017) - [c128]Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv:
Verifying Equivalence of Spark Programs. CAV (2) 2017: 282-300 - [c127]Nikolaj S. Bjørner, Maria-Cristina V. Marinescu, Mooly Sagiv:
Abduction for Learning Smart City Rules. GCAI 2017: 233-238 - [c126]Aurojit Panda, Mooly Sagiv, Scott Shenker:
Verification in the Age of Microservices. HotOS 2017: 30-36 - [c125]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: 16:1-16:18 - [c124]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Reachability in Networks with Mutable Datapaths. NSDI 2017: 699-718 - [c123]Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Bounded Quantifier Instantiation for Checking Inductive Invariants. TACAS (1) 2017: 76-95 - [c122]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: 209-227 - [c121]Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv:
Conjunctive Abstract Interpretation Using Paramodulation. VMCAI 2017: 442-461 - [i11]Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner:
Modular Safety Verification for Stateful Networks. CoRR abs/1708.05904 (2017) - [i10]Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh:
Verifying Properties of Binarized Deep Neural Networks. CoRR abs/1709.06662 (2017) - [i9]Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham:
Paxos Made EPR: Decidable Reasoning about Distributed Protocols. CoRR abs/1710.07191 (2017) - [i8]Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham:
Bounded Quantifier Instantiation for Checking Inductive Invariants. CoRR abs/1710.08668 (2017) - 2016
- [c120]Mooly Sagiv:
Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). FSTTCS 2016: 2:1-2:1 - [c119]Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham:
Ivy: safety verification by interactive generalization. PLDI 2016: 614-630 - [c118]Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv:
Decidability of inferring inductive invariants. POPL 2016: 217-231 - [c117]Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham:
Some Complexity Results for Stateful Network Verification. TACAS 2016: 811-830 - [i7]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Reachability in Networks with Mutable Datapaths. CoRR abs/1607.00991 (2016) - [i6]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 abs/1610.02101 (2016) - 2015
- [c116]Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv:
Composing concurrency control. PLDI 2015: 240-249 - [c115]Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham:
Decentralizing SDN Policies. POPL 2015: 663-676 - [c114]Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav:
Automatic scalable atomicity via semantic locking. PPoPP 2015: 31-41 - [c113]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: 252-274 - [c112]Aurojit Panda, Katerina J. Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker:
New Directions for Network Verification. SNAPL 2015: 209-220 - 2014
- [c111]Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur:
Property-Directed Shape Analysis. CAV 2014: 35-51 - [c110]Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv:
Checking Linearizability of Encapsulated Extended Operations. ESOP 2014: 311-330 - [c109]Ohad Shacham, Eran Yahav, Guy Golan-Gueta, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv, Martin T. Vechev:
Verifying atomicity via data independence. ISSTA 2014: 26-36 - [c108]Thomas Ball, Nikolaj S. 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: 282-293 - [c107]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv:
Modular reasoning about heap paths via effectively propositional formulas. POPL 2014: 385-396 - [c106]Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav:
Automatic semantic locking. PPoPP 2014: 385-386 - [i5]Aurojit Panda, Ori Lahav, Katerina J. Argyraki, Mooly Sagiv, Scott Shenker:
Verifying Isolation Properties in the Presence of Middleboxes. CoRR abs/1409.7687 (2014) - 2013
- [j25]Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler:
Principles of POPL. ACM SIGPLAN Notices 48(4S): 12-16 (2013) - [c105]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: 414-445 - [c104]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv:
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV 2013: 756-772 - [c103]Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv:
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. LPAR 2013: 457-472 - [c102]Omer Tripp, Eric Koskinen, Mooly Sagiv:
Turning nondeterminism into parallelism. OOPSLA 2013: 589-604 - [c101]Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv, Eran Yahav:
Concurrent libraries with foresight. PLDI 2013: 263-274 - [c100]Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv:
Synthesis of Circular Compositional Program Proofs via Abduction. TACAS 2013: 370-384 - 2012
- [j24]Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher:
An introduction to data representation synthesis. Commun. ACM 55(12): 91-99 (2012) - [j23]Mooly Sagiv:
POPL'11 program chair's report. ACM SIGPLAN Notices 47(4a): 16-18 (2012) - [c99]Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, Mooly Sagiv:
Eventually Consistent Transactions. ESOP 2012: 67-86 - [c98]Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv:
Reasoning about Lock Placements. ESOP 2012: 336-356 - [c97]Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv:
Understanding the behavior of database operations under program control. OOPSLA 2012: 983-996 - [c96]Omer Tripp, Roman Manevich, John Field, Mooly Sagiv:
JANUS: exploiting parallelism via hindsight. PLDI 2012: 145-156 - [c95]Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv:
Concurrent data representation synthesis. PLDI 2012: 417-428 - [c94]Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv:
Abstractions from tests. POPL 2012: 373-386 - 2011
- [c93]Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav:
Testing atomicity of composed concurrent operations. OOPSLA 2011: 51-64 - [c92]Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv:
HAWKEYE: effective discovery of dataflow impediments to parallelization. OOPSLA 2011: 207-224 - [c91]Guy Golan-Gueta, Nathan Grasso Bronson, Alex Aiken, G. Ramalingam, Mooly Sagiv, Eran Yahav:
Automatic fine-grain locking using shape properties. OOPSLA 2011: 225-242 - [c90]Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv:
Data representation synthesis. PLDI 2011: 38-49 - [c89]Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv:
Precise and compact modular procedure summaries for heap manipulating programs. PLDI 2011: 567-577 - [e5]Thomas Ball, Mooly Sagiv:
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. ACM 2011, ISBN 978-1-4503-0490-0 [contents] - 2010
- [j22]Aharon Abadi, Alexander Rabinovich, Mooly Sagiv:
Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2): 153-172 (2010) - [j21]Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv:
A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. 32(2): 5:1-5:52 (2010) - [j20]Eran Yahav, Mooly Sagiv:
Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5): 18:1-18:50 (2010) - [j19]Thomas W. Reps, Mooly Sagiv, Alexey Loginov:
Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 32(6): 24:1-24:55 (2010) - [c88]Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv:
Data Structure Fusion. APLAS 2010: 204-221 - [c87]Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv:
Specifying and verifying sparse matrix codes. ICFP 2010: 249-260 - [c86]Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv:
A simple inductive synthesis methodology and its applications. OOPSLA 2010: 36-46 - [c85]Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv:
A dynamic evaluation of the precision of static heap abstractions. OOPSLA 2010: 411-427 - [c84]Bill McCloskey, Thomas W. Reps, Mooly Sagiv:
Statically Inferring Complex Heap, Array, and Numeric Invariants. SAS 2010: 71-99 - [c83]Shay Litvak, Nurit Dor, Rastislav Bodík, Noam Rinetzky, Mooly Sagiv:
Field-sensitive program dependence analysis. SIGSOFT FSE 2010: 287-296
2000 – 2009
- 2009
- [j18]Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Mooly Sagiv, Siddharth Srivastava, Greta Yorsh:
Simulating reachability using first-order logic with applications to verification of linked data structures. Log. Methods Comput. Sci. 5(2) (2009) - [j17]Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv:
Self-stabilization preserving compiler. ACM Trans. Program. Lang. Syst. 31(6): 22:1-22:42 (2009) - [c82]Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv:
Abstract Transformers for Thread Correlation Analysis. APLAS 2009: 30-46 - [c81]Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv:
Generalizing DPLL to Richer Logics. CAV 2009: 462-476 - [c80]Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv:
A combination framework for tracking partition sizes. POPL 2009: 239-251 - [c79]Mooly Sagiv:
Thread-Modular Shape Analysis. VMCAI 2009: 3 - [e4]Peter W. O'Hearn, Arnd Poetzsch-Heffter, Mooly Sagiv:
Typing, Analysis and Verification of Heap-Manipulating Programs, 19.07. - 24.07.2009. Dagstuhl Seminar Proceedings 09301, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2009 [contents] - [i4]Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn:
09301 Abstracts Collection - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs 2009 - [i3]Mooly Sagiv, Arnd Poetzsch-Heffter, Peter W. O'Hearn:
09301 Executive Summary - Typing, Analysis, and Verification of Heap-Manipulating Programs. Typing, Analysis and Verification of Heap-Manipulating Programs 2009 - 2008
- [j16]Noam Rinetzky, G. Ramalingam, Shmuel Sagiv, Eran Yahav:
On the complexity of partially-flow-sensitive alias analysis. ACM Trans. Program. Lang. Syst. 30(3): 13:1-13:28 (2008) - [c78]Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv:
Proving Conditional Termination. CAV 2008: 328-340 - [c77]Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv:
Thread Quantification for Concurrent Shape Analysis. CAV 2008: 399-413 - [c76]Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang:
Ranking Abstractions. ESOP 2008: 148-162 - [c75]Nurit Dor, Tal Lev-Ami, Shay Litvak, Mooly Sagiv, Dror Weiss:
Customization change impact analysis for erp professionals via program slicing. ISSTA 2008: 97-108 - [c74]Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine:
Heap Decomposition for Concurrent Shape Analysis. SAS 2008: 363-377 - 2007
- [j15]Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani:
A logic of reachable patterns in linked data-structures. J. Log. Algebraic Methods Program. 73(1-2): 111-142 (2007) - [j14]Ohad Shacham, Mooly Sagiv, Assaf Schuster:
Scaling model checking of dataraces using dynamic information. J. Parallel Distributed Comput. 67(5): 536-550 (2007) - [j13]Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm:
Logical characterizations of heap abstractions. ACM Trans. Comput. Log. 8(1): 5 (2007) - [j12]Mooly Sagiv:
Introduction to special ESOP'05 issue. ACM Trans. Program. Lang. Syst. 29(5): 23 (2007) - [c73]Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv:
Local Reasoning for Storable Locks and Threads. APLAS 2007: 19-37 - [c72]Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv:
Labelled Clauses. CADE 2007: 311-327 - [c71]Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv:
Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV 2007: 221-225 - [c70]Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav:
Comparison Under Abstraction for Verifying Linearizability. CAV 2007: 477-490 - [c69]Thomas Ball, Orna Kupferman, Mooly Sagiv:
Leaping Loops in the Presence of Abstraction. CAV 2007: 491-503 - [c68]Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav:
Modular Shape Analysis for Dynamically Encapsulated Programs. ESOP 2007: 220-236 - [c67]Aharon Abadi, Alexander Moshe Rabinovich, Mooly Sagiv:
Decidable Fragments of Many-Sorted Logic. LPAR 2007: 17-31 - [c66]Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv:
Thread-modular shape analysis. PLDI 2007: 266-277 - [c65]Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv:
Cartesian Partial-Order Reduction. SPIN 2007: 95-112 - [c64]Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv:
Shape Analysis by Graph Decomposition. TACAS 2007: 3-18 - [c63]Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps:
Constructing Specialized Shape Analyses for Uniform Change. VMCAI 2007: 215-233 - [p2]Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm:
Shape Analysis and Applications. The Compiler Design Handbook, 2nd ed. 2007: 12 - [e3]Thomas W. Reps, Mooly Sagiv, Jörg Bauer:
Program Analysis and Compilation, Theory and Practice, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 4444, Springer 2007, ISBN 978-3-540-71315-9 [contents] - [e2]Greg Morrisett, Mooly Sagiv:
Proceedings of the 6th International Symposium on Memory Management, ISMM 2007, Montreal, Quebec, Canada, October 21-22, 2007. ACM 2007, ISBN 978-1-59593-893-0 [contents] - [i2]Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani:
A Logic of Reachable Patterns in Linked Data-Structures. CoRR abs/0705.3610 (2007) - 2006
- [j11]Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
Verifying Temporal Heap Properties Specified via Evolution Logic. Log. J. IGPL 14(5): 755-783 (2006) - [j10]Danny Nebenzahl, Shmuel Sagiv, Avishai Wool:
Install-Time Vaccination of Windows Executables to Defend against Stack Smashing Attacks. IEEE Trans. Dependable Secur. Comput. 3(1): 78-90 (2006) - [c62]Thomas W. Reps, Mooly Sagiv, Jörg Bauer:
An Appreciation of the Work of Reinhard Wilhelm. Program Analysis and Compilation 2006: 1-11 - [c61]Alexey Loginov, Thomas W. Reps, Mooly Sagiv:
Refinement-Based Verification for Possibly-Cyclic Lists. Program Analysis and Compilation 2006: 247-272 - [c60]Roman Manevich, John Field, Thomas A. Henzinger, G. Ramalingam, Mooly Sagiv:
Abstract Counterexample-Based Refinement for Powerset Domains. Program Analysis and Compilation 2006: 273-292 - [c59]Tal Lev-Ami, Neil Immerman, Shmuel Sagiv:
Abstraction for Shape Analysis with Fast and Precise Transformers. CAV 2006: 547-561 - [c58]Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani:
A Logic of Reachable Patterns in Linked Data-Structures. FoSSaCS 2006: 94-110 - [c57]Greta Yorsh, Thomas Ball, Mooly Sagiv:
Testing, abstraction, theorem proving: better together! ISSTA 2006: 145-156 - [c56]Alexey Loginov, Thomas W. Reps, Mooly Sagiv:
Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. SAS 2006: 261-279 - [c55]Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham:
Combining Shape Analyses by Intersecting Abstractions. VMCAI 2006: 33-48 - 2005
- [j9]Ran Shaham, Eran Yahav, Elliot K. Kolodner, Mooly Sagiv:
Establishing local temporal heap safety properties with applications to compile-time memory management. Sci. Comput. Program. 58(1-2): 264-289 (2005) - [c54]Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh:
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. CADE 2005: 99-115 - [c53]Alexey Loginov, Thomas W. Reps, Shmuel Sagiv:
Abstraction Refinement via Inductive Learning. CAV 2005: 519-533 - [c52]Yair Sade, Shmuel Sagiv, Ran Shaham:
Optimizing C Multithreaded Memory Management Using Thread-Local Storage. CC 2005: 137-155 - [c51]Noam Rinetzky, Jörg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
A semantics for procedure local heaps and its abstractions. POPL 2005: 296-309 - [c50]Denis Gopan, Thomas W. Reps, Shmuel Sagiv:
A framework for numeric analysis of array operations. POPL 2005: 338-350 - [c49]Ohad Shacham, Mooly Sagiv, Assaf Schuster:
Scaling model checking of dataraces using dynamic information. PPoPP 2005: 107-118 - [c48]Noam Rinetzky, Mooly Sagiv, Eran Yahav:
Interprocedural Shape Analysis for Cutpoint-Free Programs. SAS 2005: 284-302 - [c47]Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv:
Self-stabilization Preserving Compiler. Self-Stabilizing Systems 2005: 81-95 - [c46]Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv:
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. VMCAI 2005: 181-198 - [c45]Nurit Dor, John Field, Denis Gopan, Tal Lev-Ami, Alexey Loginov, Roman Manevich, G. Ramalingam, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav, Greta Yorsh:
Automatic Verification of Strongly Dynamic Software Systems. VSTTE 2005: 82-92 - [c44]Greta Yorsh, Alexey Skidanov, Thomas W. Reps, Shmuel Sagiv:
Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work. AIOOL@VMCAI 2005: 125-138 - [e1]Shmuel Sagiv:
Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings. Lecture Notes in Computer Science 3444, Springer 2005, ISBN 3-540-25435-8 [contents] - 2004
- [c43]Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
Static Program Analysis via 3-Valued Logic. CAV 2004: 15-30 - [c42]Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
Verification via Structure Simulation. CAV 2004: 281-294 - [c41]Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. CSL 2004: 160-174 - [c40]Tal Lev-Ami, Roman Manevich, Shmuel Sagiv:
TVLA: A system for generating abstract interpreters. IFIP Congress Topical Sessions 2004: 367-375 - [c39]Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv:
A Relational Approach to Interprocedural Shape Analysis. SAS 2004: 246-264 - [c38]Roman Manevich, Shmuel Sagiv, Ganesan Ramalingam, John Field:
Partially Disjunctive Heap Abstraction. SAS 2004: 265-279 - [c37]Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv:
Numeric Domains with Summarized Dimensions. TACAS 2004: 512-529 - [c36]Greta Yorsh, Thomas W. Reps, Shmuel Sagiv:
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. TACAS 2004: 530-545 - [c35]Shmuel Sagiv:
On the Expressive Power of Canonical Abstraction. VMCAI 2004: 58 - [c34]Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
Symbolic Implementation of the Best Transformer. VMCAI 2004: 252-266 - 2003
- [c33]Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
Verifying Temporal Heap Properties Specified via Evolution Logic. ESOP 2003: 204-222 - [c32]Thomas W. Reps, Shmuel Sagiv, Alexey Loginov:
Finite Differencing of Logical Formulas for Static Analysis. ESOP 2003: 380-398 - [c31]Nurit Dor, Michael Rodeh, Shmuel Sagiv:
CSSV: towards a realistic tool for statically detecting all buffer overflows in C. PLDI 2003: 155-167 - [c30]Ran Shaham, Eran Yahav, Elliot K. Kolodner, Shmuel Sagiv:
Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management. SAS 2003: 483-503 - [c29]Eran Yahav, Shmuel Sagiv:
Automatically Verifying Concurrent Queue Algorithms. SoftMC@CAV 2003: 450-463 - [i1]Greta Yorsh, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
Logical Characterizations of Heap Abstractions. CoRR cs.LO/0312014 (2003) - 2002
- [j8]Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm:
Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3): 217-298 (2002) - [c28]David Oren, Yossi Matias, Shmuel Sagiv:
Online Subpath Profiling. CC 2002: 78-94 - [c27]Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv:
Estimating the impact of heap liveness information on space consumption in Java. MSP/ISMM 2002: 171-182 - [c26]Thomas W. Reps, Alexey Loginov, Shmuel Sagiv:
Semantic Minimization of 3-Valued Propositional Formulae. LICS 2002: 40- - [c25]G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, Shmuel Sagiv:
Deriving Specialized Program Analyses for Certifying Component-Client Conformance. PLDI 2002: 83-94 - [c24]Roman Manevich, G. Ramalingam, John Field, Deepak Goyal, Shmuel Sagiv:
Compactly Representing First-Order Structures for Static Analysis. SAS 2002: 196-212 - [p1]Reinhard Wilhelm, Thomas W. Reps, Shmuel Sagiv:
Shape Analysis and Applications. The Compiler Design Handbook 2002: 175-218 - 2001
- [j7]Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv:
Kleene's Logic with Equality. Inf. Process. Lett. 80(3): 131-137 (2001) - [c23]Noam Rinetzky, Shmuel Sagiv:
Interprocedural Shape Analysis for Recursive Programs. CC 2001: 133-149 - [c22]Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv:
Heap Profiling for Space-Efficient Java. PLDI 2001: 104-113 - [c21]Nurit Dor, Michael Rodeh, Shmuel Sagiv:
Cleanness Checking of String Manipulations in C Programs via Integer Analysis. SAS 2001: 194-212 - 2000
- [c20]Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps:
Shape Analysis. CC 2000: 1-17 - [c19]Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv:
Automatic Removal of Array Memory Leaks in Java. CC 2000: 50-66 - [c18]Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv:
A Kleene Analysis of Mobile Ambients. ESOP 2000: 305-319 - [c17]Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
Putting static analysis to work for verification: A case study. ISSTA 2000: 26-38 - [c16]Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv:
On the Effectiveness of GC in Java. ISMM 2000: 12-17 - [c15]Nurit Dor, Michael Rodeh, Shmuel Sagiv:
Checking Cleanness in Linked Lists. SAS 2000: 115-134 - [c14]Tal Lev-Ami, Shmuel Sagiv:
TVLA: A System for Implementing Static Analyses. SAS 2000: 280-301
1990 – 1999
- 1999
- [j6]Michael Rodeh, Shmuel Sagiv:
Finding Circular Attributes in Attribute Grammars. J. ACM 46(4): 556 (1999) - [c13]Michael Benedikt, Thomas W. Reps, Shmuel Sagiv:
A Decidable Logic for Describing Linked Data Structures. ESOP 1999: 2-19 - [c12]Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm:
Parametric Shape Analysis via 3-Valued Logic. POPL 1999: 105-118 - 1998
- [j5]Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm:
A Logic-Based Approach to Program Flow Analysis. Acta Informatica 35(6): 457-504 (1998) - [j4]John L. Ross, Shmuel Sagiv:
Building a Bridge between Pointer Aliases and Program Dependences. Nord. J. Comput. 5(4): 361- (1998) - [j3]Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm:
Solving Shape-Analysis Problems in Languages with Destructive Updating. ACM Trans. Program. Lang. Syst. 20(1): 1-50 (1998) - [c11]John L. Ross, Shmuel Sagiv:
Building a Bridge between Pointer Aliases and Program Dependences. ESOP 1998: 221-235 - [c10]Nurit Dor, Michael Rodeh, Shmuel Sagiv:
Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience). PASTE 1998: 27-34 - [c9]Thomas Ball, Peter Mataga, Shmuel Sagiv:
Edge Profiling versus Path Profiling: The Showdown. POPL 1998: 134-148 - 1996
- [j2]Shmuel Sagiv, Thomas W. Reps, Susan Horwitz:
Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theor. Comput. Sci. 167(1&2): 131-170 (1996) - [c8]Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm:
Solving Shape-Analysis Problems in Languages with Destructive Updating. POPL 1996: 16-31 - 1995
- [c7]Thomas W. Reps, Susan Horwitz, Shmuel Sagiv:
Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995: 49-61 - [c6]Susan Horwitz, Thomas W. Reps, Shmuel Sagiv:
Demand Interprocedural Dataflow Analysis. SIGSOFT FSE 1995: 104-115 - [c5]Shmuel Sagiv, Thomas W. Reps, Susan Horwitz:
Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. TAPSOFT 1995: 651-665 - 1994
- [c4]Thomas W. Reps, Susan Horwitz, Shmuel Sagiv, Genevieve Rosay:
Speeding up Slicing. SIGSOFT FSE 1994: 11-20 - 1992
- [j1]Johann A. Makowsky, J.-C. Gregoire, Shmuel Sagiv:
The Expressive Power of Side Effects in Prolog. J. Log. Program. 12(1&2): 179-188 (1992) - [c3]David Bernstein, Michael Rodeh, Shmuel Sagiv:
Proving Safety of Speculative Load Instructions at Compile Time. ESOP 1992: 56-72 - 1991
- [b1]Shmuel Sagiv:
High level formalisms for program flow analysis and their use in compiling. Technion - Israel Institute of Technology, Israel, 1991 - 1990
- [c2]Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm:
A Logic-Based Approach to Data Flow Analysis Problem. PLILP 1990: 277-292
1980 – 1989
- 1989
- [c1]Shmuel Sagiv, Orit Edelstein, Nissim Francez, Michael Rodeh:
Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis. POPL 1989: 36-48
Coauthor Index
Guy Golan-Gueta
aka: Guy Gueta
aka: Guy Gueta
Alexander Moshe Rabinovich
aka: Alexander Rabinovich
aka: Alexander Rabinovich
G. Ramalingam
aka: Ganesan Ramalingam
aka: Ganesan Ramalingam
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-22 20:42 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
