Shmuel Sagiv

Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, Mooly Sagiv: Synthesis of Circular Compositional Program Proofs via Abduction. TACAS 2013: 370-384

Peter Hawkins, Martin C. Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher: An introduction to data representation synthesis. Commun. ACM 55(12): 91-99 (2012)

Sebastian Burckhardt, Daan Leijen, Manuel Fähndrich, Mooly Sagiv: Eventually Consistent Transactions. ESOP 2012: 67-86

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv: Reasoning about Lock Placements. ESOP 2012: 336-356

Juan M. Tamayo, Alex Aiken, Nathan Grasso Bronson, Mooly Sagiv: Understanding the behavior of database operations under program control. OOPSLA 2012: 983-996

Omer Tripp, Roman Manevich, John Field, Mooly Sagiv: JANUS: exploiting parallelism via hindsight. PLDI 2012: 145-156

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv: Concurrent data representation synthesis. PLDI 2012: 417-428

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv: Abstractions from tests. POPL 2012: 373-386

Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, Eran Yahav: Testing atomicity of composed concurrent operations. OOPSLA 2011: 51-64

Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv: HAWKEYE: effective discovery of dataflow impediments to parallelization. OOPSLA 2011: 207-224

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

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv: Data representation synthesis. PLDI 2011: 38-49

Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv: Precise and compact modular procedure summaries for heap manipulating programs. PLDI 2011: 567-577

Thomas Ball, Mooly Sagiv (Eds.): 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

Aharon Abadi, Alexander Rabinovich, Mooly Sagiv: Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2): 153-172 (2010)

Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Mooly Sagiv: A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. 32(2) (2010)

Eran Yahav, Mooly Sagiv: Verifying safety properties of concurrent heap-manipulating programs. ACM Trans. Program. Lang. Syst. 32(5) (2010)

Thomas W. Reps, Mooly Sagiv, Alexey Loginov: Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 32(6) (2010)

Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv: Data Structure Fusion. APLAS 2010: 204-221

Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, Mooly Sagiv: Specifying and verifying sparse matrix codes. ICFP 2010: 249-260

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv: A simple inductive synthesis methodology and its applications. OOPSLA 2010: 36-46

Percy Liang, Omer Tripp, Mayur Naik, Mooly Sagiv: A dynamic evaluation of the precision of static heap abstractions. OOPSLA 2010: 411-427

Bill McCloskey, Thomas W. Reps, Mooly Sagiv: Statically Inferring Complex Heap, Array, and Numeric Invariants. SAS 2010: 71-99

Shay Litvak, Nurit Dor, Rastislav Bodík, Noam Rinetzky, Mooly Sagiv: Field-sensitive program dependence analysis. SIGSOFT FSE 2010: 287-296

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. Logical Methods in Computer Science 5(2) (2009)

Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv: Self-stabilization preserving compiler. ACM Trans. Program. Lang. Syst. 31(6) (2009)

Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv: Abstract Transformers for Thread Correlation Analysis. APLAS 2009: 30-46

Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv: Generalizing DPLL to Richer Logics. CAV 2009: 462-476

Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv: A combination framework for tracking partition sizes. POPL 2009: 239-251

Mooly Sagiv: Thread-Modular Shape Analysis. VMCAI 2009: 3

Noam Rinetzky, G. Ramalingam, Shmuel Sagiv, Eran Yahav: On the complexity of partially-flow-sensitive alias analysis. ACM Trans. Program. Lang. Syst. 30(3) (2008)

Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv: Proving Conditional Termination. CAV 2008: 328-340

Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv: Thread Quantification for Concurrent Shape Analysis. CAV 2008: 399-413

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang: Ranking Abstractions. ESOP 2008: 148-162

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

Roman Manevich, Tal Lev-Ami, Mooly Sagiv, Ganesan Ramalingam, Josh Berdine: Heap Decomposition for Concurrent Shape Analysis. SAS 2008: 363-377

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. 73(1-2): 111-142 (2007)

Ohad Shacham, Mooly Sagiv, Assaf Schuster: Scaling model checking of dataraces using dynamic information. J. Parallel Distrib. Comput. 67(5): 536-550 (2007)

Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm: Logical characterizations of heap abstractions. ACM Trans. Comput. Log. 8(1) (2007)

Mooly Sagiv: Introduction to special ESOP'05 issue. ACM Trans. Program. Lang. Syst. 29(5) (2007)

Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm: Shape Analysis and Applications. The Compiler Design Handbook, 2nd ed. 2007: 12

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv: Local Reasoning for Storable Locks and Threads. APLAS 2007: 19-37

Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv: Labelled Clauses. CADE 2007: 311-327

Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv: Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV 2007: 221-225

Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav: Comparison Under Abstraction for Verifying Linearizability. CAV 2007: 477-490

Thomas Ball, Orna Kupferman, Mooly Sagiv: Leaping Loops in the Presence of Abstraction. CAV 2007: 491-503

Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav: Modular Shape Analysis for Dynamically Encapsulated Programs. ESOP 2007: 220-236

Aharon Abadi, Alexander Moshe Rabinovich, Mooly Sagiv: Decidable Fragments of Many-Sorted Logic. LPAR 2007: 17-31

Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv: Thread-modular shape analysis. PLDI 2007: 266-277

Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv: Cartesian Partial-Order Reduction. SPIN 2007: 95-112

Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv: Shape Analysis by Graph Decomposition. TACAS 2007: 3-18

Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps: Constructing Specialized Shape Analyses for Uniform Change. VMCAI 2007: 215-233

Thomas W. Reps, Mooly Sagiv, Jörg Bauer (Eds.): 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

Greg Morrisett, Mooly Sagiv (Eds.): 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

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)

Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Verifying Temporal Heap Properties Specified via Evolution Logic. Logic Journal of the IGPL 14(5): 755-783 (2006)

Danny Nebenzahl, Shmuel Sagiv, Avishai Wool: Install-Time Vaccination of Windows Executables to Defend against Stack Smashing Attacks. IEEE Trans. Dependable Sec. Comput. 3(1): 78-90 (2006)

Thomas W. Reps, Mooly Sagiv, Jörg Bauer: An Appreciation of the Work of Reinhard Wilhelm. Program Analysis and Compilation 2006: 1-11

Alexey Loginov, Thomas W. Reps, Mooly Sagiv: Refinement-Based Verification for Possibly-Cyclic Lists. Program Analysis and Compilation 2006: 247-272

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

Tal Lev-Ami, Neil Immerman, Shmuel Sagiv: Abstraction for Shape Analysis with Fast and Precise Transformers. CAV 2006: 547-561

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani: A Logic of Reachable Patterns in Linked Data-Structures. FoSSaCS 2006: 94-110

Greta Yorsh, Thomas Ball, Mooly Sagiv: Testing, abstraction, theorem proving: better together! ISSTA 2006: 145-156

Alexey Loginov, Thomas W. Reps, Mooly Sagiv: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. SAS 2006: 261-279

Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham: Combining Shape Analyses by Intersecting Abstractions. VMCAI 2006: 33-48

Greta Yorsh, Alexey Skidanov, Thomas W. Reps, Shmuel Sagiv: Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work. Electr. Notes Theor. Comput. Sci. 131: 125-138 (2005)

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)

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

Alexey Loginov, Thomas W. Reps, Shmuel Sagiv: Abstraction Refinement via Inductive Learning. CAV 2005: 519-533

Yair Sade, Shmuel Sagiv, Ran Shaham: Optimizing C Multithreaded Memory Management Using Thread-Local Storage. CC 2005: 137-155

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

Denis Gopan, Thomas W. Reps, Shmuel Sagiv: A framework for numeric analysis of array operations. POPL 2005: 338-350

Ohad Shacham, Mooly Sagiv, Assaf Schuster: Scaling model checking of dataraces using dynamic information. PPOPP 2005: 107-118

Noam Rinetzky, Mooly Sagiv, Eran Yahav: Interprocedural Shape Analysis for Cutpoint-Free Programs. SAS 2005: 284-302

Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv: Self-stabilization Preserving Compiler. Self-Stabilizing Systems 2005: 81-95

Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. VMCAI 2005: 181-198

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

Shmuel Sagiv (Ed.): 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

Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Static Program Analysis via 3-Valued Logic. CAV 2004: 15-30

Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh: Verification via Structure Simulation. CAV 2004: 281-294

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

Tal Lev-Ami, Roman Manevich, Shmuel Sagiv: TVLA: A system for generating abstract interpreters. IFIP Congress Topical Sessions 2004: 367-376

Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv: A Relational Approach to Interprocedural Shape Analysis. SAS 2004: 246-264

Roman Manevich, Shmuel Sagiv, Ganesan Ramalingam, John Field: Partially Disjunctive Heap Abstraction. SAS 2004: 265-279

Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv: Numeric Domains with Summarized Dimensions. TACAS 2004: 512-529

Greta Yorsh, Thomas W. Reps, Shmuel Sagiv: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. TACAS 2004: 530-545

Shmuel Sagiv: On the Expressive Power of Canonical Abstraction. VMCAI 2004: 58

Thomas W. Reps, Shmuel Sagiv, Greta Yorsh: Symbolic Implementation of the Best Transformer. VMCAI 2004: 252-266

Eran Yahav, Shmuel Sagiv: Automatically Verifying Concurrent Queue Algorithms. Electr. Notes Theor. Comput. Sci. 89(3): 450-463 (2003)

Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Verifying Temporal Heap Properties Specified via Evolution Logic. ESOP 2003: 204-222

Thomas W. Reps, Shmuel Sagiv, Alexey Loginov: Finite Differencing of Logical Formulas for Static Analysis. ESOP 2003: 380-398

Nurit Dor, Michael Rodeh, Shmuel Sagiv: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. PLDI 2003: 155-167

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

Greta Yorsh, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Logical Characterizations of Heap Abstractions. CoRR cs.LO/0312014 (2003)

Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3): 217-298 (2002)

Reinhard Wilhelm, Thomas W. Reps, Shmuel Sagiv: Shape Analysis and Applications. The Compiler Design Handbook 2002: 175-218

David Oren, Yossi Matias, Shmuel Sagiv: Online Subpath Profiling. CC 2002: 78-94

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv: Estimating the impact of heap liveness information on space consumption in Java. MSP/ISMM 2002: 171-182

Thomas W. Reps, Alexey Loginov, Shmuel Sagiv: Semantic Minimization of 3-Valued Propositional Formulae. LICS 2002: 40-

G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, Shmuel Sagiv: Deriving Specialized Program Analyses for Certifying Component-Client Conformance. PLDI 2002: 83-94

Roman Manevich, G. Ramalingam, John Field, Deepak Goyal, Shmuel Sagiv: Compactly Representing First-Order Structures for Static Analysis. SAS 2002: 196-212

Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv: Kleene's Logic with Equality. Inf. Process. Lett. 80(3): 131-137 (2001)

Noam Rinetzky, Shmuel Sagiv: Interprocedural Shape Analysis for Recursive Programs. CC 2001: 133-149

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv: Heap Profiling for Space-Efficient Java. PLDI 2001: 104-113

Nurit Dor, Michael Rodeh, Shmuel Sagiv: Cleanness Checking of String Manipulations in C Programs via Integer Analysis. SAS 2001: 194-212

Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps: Shape Analysis. CC 2000: 1-17

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv: Automatic Removal of Array Memory Leaks in Java. CC 2000: 50-66

Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv: A Kleene Analysis of Mobile Ambients. ESOP 2000: 305-319

Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm: Putting static analysis to work for verification: A case study. ISSTA 2000: 26-38

Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv: On the Effectiveness of GC in Java. ISMM 2000: 12-17

Nurit Dor, Michael Rodeh, Shmuel Sagiv: Checking Cleanness in Linked Lists. SAS 2000: 115-134

Tal Lev-Ami, Shmuel Sagiv: TVLA: A System for Implementing Static Analyses. SAS 2000: 280-301

Michael Rodeh, Shmuel Sagiv: Finding Circular Attributes in Attribute Grammars. J. ACM 46(4): 556 (1999)

Michael Benedikt, Thomas W. Reps, Shmuel Sagiv: A Decidable Logic for Describing Linked Data Structures. ESOP 1999: 2-19

Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm: Parametric Shape Analysis via 3-Valued Logic. POPL 1999: 105-118

Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm: A Logic-Based Approach to Program Flow Analysis. Acta Inf. 35(6): 457-504 (1998)

John L. Ross, Shmuel Sagiv: Building a Bridge between Pointer Aliases and Program Dependences. Nord. J. Comput. 5(4): 361- (1998)

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)

John L. Ross, Shmuel Sagiv: Building a Bridge between Pointer Aliases and Program Dependences. ESOP 1998: 221-235

Nurit Dor, Michael Rodeh, Shmuel Sagiv: Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience). PASTE 1998: 27-34

Thomas Ball, Peter Mataga, Shmuel Sagiv: Edge Profiling versus Path Profiling: The Showdown. POPL 1998: 134-148

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)

Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm: Solving Shape-Analysis Problems in Languages with Destructive Updating. POPL 1996: 16-31

Thomas W. Reps, Susan Horwitz, Shmuel Sagiv: Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995: 49-61

Susan Horwitz, Thomas W. Reps, Shmuel Sagiv: Demand Interprocedural Dataflow Analysis. SIGSOFT FSE 1995: 104-115

Shmuel Sagiv, Thomas W. Reps, Susan Horwitz: Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. TAPSOFT 1995: 651-665

Thomas W. Reps, Susan Horwitz, Shmuel Sagiv, Genevieve Rosay: Speeding up Slicing. SIGSOFT FSE 1994: 11-20

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)

David Bernstein, Michael Rodeh, Shmuel Sagiv: Proving Safety of Speculative Load Instructions at Compile Time. ESOP 1992: 56-72

Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm: A Logic-Based Approach to Data Flow Analysis Problem. PLILP 1990: 277-292

Shmuel Sagiv, O. Edelstein, Nissim Francez, Michael Rodeh: Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis. POPL 1989: 36-48