| 2008 | CAV | Thread Quantification for Concurrent Shape Analysis. | Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv |
| 2006 | CAV | Abstraction for Shape Analysis with Fast and Precise Transformers. | Tal Lev-Ami, Neil Immerman, Shmuel Sagiv |
| 2005 | CADE | Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. | Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh |
| 2005 | CAV | Abstraction Refinement via Inductive Learning. | Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2005 | CC | Optimizing C Multithreaded Memory Management Using Thread-Local Storage. | Yair Sade, Shmuel Sagiv, Ran Shaham |
| 2005 | POPL | A framework for numeric analysis of array operations. | Denis Gopan, Thomas W. Reps, Shmuel Sagiv |
| 2005 | POPL | A semantics for procedure local heaps and its abstractions. | Noam Rinetzky, Jrg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2005 | VMCAI | Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. | Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv |
| 2004 | CAV | Verification via Structure Simulation. | Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | CAV | Static Program Analysis via 3-Valued Logic. | Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2004 | CSL | The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. | Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | SAS | A Relational Approach to Interprocedural Shape Analysis. | Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2004 | SAS | Partially Disjunctive Heap Abstraction. | Roman Manevich, Shmuel Sagiv, Ganesan Ramalingam, John Field |
| 2004 | TACAS | Numeric Domains with Summarized Dimensions. | Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv |
| 2004 | TACAS | Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. | Greta Yorsh, Thomas W. Reps, Shmuel Sagiv |
| 2004 | VMCAI | Symbolic Implementation of the Best Transformer. | Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | VMCAI | On the Expressive Power of Canonical Abstraction. | Shmuel Sagiv |
| 2003 | ESOP | Finite Differencing of Logical Formulas for Static Analysis. | Thomas W. Reps, Shmuel Sagiv, Alexey Loginov |
| 2003 | ESOP | Verifying Temporal Heap Properties Specified via Evolution Logic. | Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2003 | PLDI | CSSV: towards a realistic tool for statically detecting all buffer overflows in C. | Nurit Dor, Michael Rodeh, Shmuel Sagiv |
| 2003 | SAS | Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management. | Ran Shaham, Eran Yahav, Elliot K. Kolodner, Shmuel Sagiv |
| 2002 | CC | Online Subpath Profiling. | David Oren, Yossi Matias, Shmuel Sagiv |
| 2002 | LICS | Semantic Minimization of 3-Valued Propositional Formulae. | Thomas W. Reps, Alexey Loginov, Shmuel Sagiv |
| 2002 | PLDI | Deriving Specialized Program Analyses for Certifying Component-Client Conformance. | G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, Shmuel Sagiv |
| 2002 | SAS | Compactly Representing First-Order Structures for Static Analysis. | Roman Manevich, G. Ramalingam, John Field, Deepak Goyal, Shmuel Sagiv |
| 2001 | CC | Interprocedural Shape Analysis for Recursive Programs. | Noam Rinetzky, Shmuel Sagiv |
| 2001 | PLDI | Heap Profiling for Space-Efficient Java. | Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv |
| 2001 | SAS | Cleanness Checking of String Manipulations in C Programs via Integer Analysis. | Nurit Dor, Michael Rodeh, Shmuel Sagiv |
| 2000 | CC | Automatic Removal of Array Memory Leaks in Java. | Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv |
| 2000 | CC | Shape Analysis. | Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps |
| 2000 | ESOP | A Kleene Analysis of Mobile Ambients. | Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv |
| 2000 | ISSTA | Putting static analysis to work for verification: A case study. | Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2000 | SAS | Checking Cleanness in Linked Lists. | Nurit Dor, Michael Rodeh, Shmuel Sagiv |
| 2000 | SAS | TVLA: A System for Implementing Static Analyses. | Tal Lev-Ami, Shmuel Sagiv |
| 1999 | ESOP | A Decidable Logic for Describing Linked Data Structures. | Michael Benedikt, Thomas W. Reps, Shmuel Sagiv |
| 1999 | POPL | Parametric Shape Analysis via 3-Valued Logic. | Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm |
| 1998 | ESOP | Building a Bridge between Pointer Aliases and Program Dependences. | John L. Ross, Shmuel Sagiv |
| 1998 | POPL | Edge Profiling versus Path Profiling: The Showdown. | Thomas Ball, Peter Mataga, Shmuel Sagiv |
| 1996 | POPL | Solving Shape-Analysis Problems in Languages with Destructive Updating. | Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm |
| 1995 | POPL | Precise Interprocedural Dataflow Analysis via Graph Reachability. | Thomas W. Reps, Susan Horwitz, Shmuel Sagiv |
| 1992 | ESOP | Proving Safety of Speculative Load Instructions at Compile Time. | David Bernstein, Michael Rodeh, Shmuel Sagiv |
| 1989 | POPL | Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis. | Shmuel Sagiv, Orit Edelstein, Nissim Francez, Michael Rodeh |