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]