Sagiv's Publications
2008
Ranking abstractions
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang
ESOP'08 [European Symposium on Programming]
[pdf]
Modular Shape Analysis for View-Serializable Libraries
N. Rinetzky, A. Bouajjani, G. Ramalingam, M. Sagiv, and E. Yahav
Submitted for publication
[pdf]
Heap Decomposition for Concurrent Shape Analysis
R. Manevich,., T. Lev-Ami, M. Sagiv, G. Ramalingam, and J. Berdine
Submitted for publication
[pdf]
A system implements this work is downloadable from here
Thread Quantification for Concurrent Shape Analysis
J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and M. Sagiv
Submitted for publication
[pdf]
Proving Conditional Termination
B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv
Submitted for publication
[pdf]
A system implements this work is downloadable from here
2007
Logical
characterizations of heap abstractions
Greta Yorsh, Thomas W. Reps, Mooly Sagiv, Reinhard Wilhelm
ACM Trans. Comput. Log. 8(1)(2007)
[pdf]
A logic of
reachable patterns in linked data-structures
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed
Bouajjani
The journal of logic and algebraic programming (1:111 - 142)(2007)
[pdf]
Scaling model
checking of dataraces using dynamic information
Ohad Shacham, Mooly Sagiv,
Journal of parallel and distributed
[pdf]
Leaping loops
in the presence of abstraction
Thomas Ball, Orna Kupferman, Mooly Sagiv
CAV 2007:491-503
[pdf]
Constructing
specialized shape analyses for uniform change
Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps
VMCAI 2007:215-233
[pdf]
Shape Analysis
by graph de
Roman Manevitch, Josh Berdine,Byron Cook,G. Ramalingam, Mooly Sagiv
TACAS'2007:3-18
[pdf]
Modular shape
analysis for dynamically encapsulated programs
Noam Rinetzky, Arnd Poetzsch-Heffter, G. Ramalingam, Mooly Sagiv, E. Yahav
ESOP'2007: 220-236
[pdf]
Thread-modular
shape analysis
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sagiv
PLDI 2007:266-277
[pdf]
Decidable
fragments of many-sorted logic
Aharon Abadi, Alexander Rabinovich, Mooly Sagiv
LPAR 2007:17-31
[pdf]
Comparison
under abstraction for verifying linearizability
Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav
CAV 2007:477-490
[pdf]
Revamping TVLA:
Making parametric shape analysis
Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv
CAV 2007:221-225
[pdf]
Labelled
Clauses
Tal Lev-Ami,Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv
CADE 2007:311-327
[pdf]
Local reasoning
for storable locks and threads
Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv
APLAS'07 (ASIAN symposium on programming languages and systems
(Singapore)
[pdf]
Cartesian
partial-order reduction
Guy Gueta,Cormac Flnagan, Eran Yahav, Mooly Sagiv
SPIN 2007: 95-112
[pdf]
On the
N.Rinetzky, G. Ramalingam, M. Sagiv, E. Yahav
Accepted to TOPLAS
[pdf]
On the utility
of canonic abstraction
Sagiv M., Reps T., Wilhelm R., Yahav E.
submitted for publication
Invited for a special issue on software tools for technology transfer
(STTT) "Program Analysis and validation"
Verifying
safety properties of concurrent Java programs using 3-valued logic
Yahav E., Sagiv M.
submitted for publication
Conditionally accepted to TOPLAS subject to a revision
2006
Abstraction for
Shape Analysis with Fast and Precise Transformers.
Tal Lev-Ami, Neil Immerman, Shmuel Sagiv
CAV 2006
[pdf]
A Logic of
Reachable Patterns in Linked Data-Structures
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed
Bouajjani
FoSSaCS 2006
[slides] [pdf]
Testing,
abstraction, theorem proving: better together!
Greta Yorsh, Thomas Ball, Mooly Sagiv
ISSTA 2006
[pdf] [slides]
Automated
Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
Alexey Loginov, Thomas W. Reps, Mooly Sagiv
SAS 2006
[pdf]
Combining Shape
Analyses by Intersecting Abstractions
Gilad Arnold, Roman Manevich, Mooly Sagiv, Ran Shaham
VMCAI 2006
[pdft]
Install-Time
Vaccination of Windows Executables to Defend against Stack Smashing Attacks
Danny Nebenzahl, Shmuel Sagiv, Avishai Wool
IEEE Trans. Dependable Sec. Comput. 3(1): 78-90 (2006)
[pdf]
Verifying
Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
Logic Journal of the IGPL 14(5): 755-783 (2006)
[abstract]
[pdf]
[slides]
2005
Simulating
Reachability Using First-Order Logic with Applications to Verification of
Linked Data Structures
Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, S. Srivastava,
Greta Yorsh
CADE 2005: 99-115
[pdf]
Abstraction
Refinement via Inductive Learning
Alexey Loginov, Thomas W. Reps, Shmuel Sagiv
CAV 2005: 519-533
[pdf]
Optimizing C
Multithreaded Memory Management Using Thread-Local Storage
Yair Sade, Shmuel Sagiv, Ran Shaham
CC 2005: 137-155
[pdf]
A semantics for
procedure local heaps and its abstractions
Noam Rinetzky, Jorg Bauer, Thomas W. Reps, Shmual Sagiv, Reinhard Wilhelm
POPL 2005: 296-309
[pdf]
A framework for
numeric analysis of array operations
Denis Gopan, Thomas W. Reps, Shmuel Sagiv
POPL 2005: 338-350
[pdf]
Scaling model
checking of dataraces using dynamic information
Ohad Shacham, Mooly Sagiv,
PPOPP 2005: 107-118
[pdf]
Interprocedural
Shape Analysis for Cutpoint-Free Programs
Noam Rinetzky, Mooly Sagiv, Eran Yahav
SAS 2005: 284-302
[pdf]
Self-stabilization
Preserving Compiler
Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv
Self-Stabilizing Systems 2005: 81-95
[pdf]
Predicate
Abstraction and Canonical Abstraction for Singly-Linked Lists
Roman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv
VMCAI 2005: 181-198
[pdf]
Automatic
Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work
Greta Yorsh, Alexey Skidanov, Thomas W. Reps, Shmuel Sagiv
Electr. Notes Theor. Comput. Sci. 131: 125-138 (2005)
[pdf]
Establishing
local temporal heap safety properties with applications to
Ran Shaham, Eran Yahav, Elliot K. Kolodner, Mooly Sagiv
Sci. Comput. Program. 58(1-2): 264-289 (2005)
[pdf]
Automatic
verification of strongly dynamic software systems
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
In Proc. IFIP working conference on verified software: Theories, Tools,
Experiments, Zurich, Switzerland, Oct.10-13, 2005
[pdf]
2004
Static Program
Analysis via 3-Valued Logic
Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
CAV 2004: 15-30
[pdf]
Verification
via Structure Simulation
Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv,
Greta Yorsh
CAV 2004: 281-294
[pdf]
The Boundary
Between Decidability and Undecidability for Transitive-Closure Logics
Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv,
Greta Yorsh
CSL 2004: 160-174
[pdf]
TVLA: A system
for generating abstract interpreters
Tal Lev-Ami, Roman Manevich, Shmuel Sagiv
IFIP Congress Topical Sessions 2004: 367-376
[pdf]
A Relational
Approach to Interprocedural Shape Analysis
Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv
SAS 2004: 246-264
[pdf]
Partially
Disjunctive Heap Abstraction
Roman Manevich, Shmuel Sagiv, Ganesan Ramalingam, John Field
SAS 2004: 265-279
[pdf]
Numeric Domains
with Summarized Dimensions
Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv
TACAS 2004: 512-529
[pdf]
Symbolically
Computing Most-Precise Abstract Operations for Shape Analysis
Greta Yorsh, Thomas W. Reps, Shmuel Sagiv
TACAS 2004: 530-545
[pdf]
Symbolic
Implementation of the Best Transformer
Thomas W. Reps, Shmuel Sagiv, Greta Yorsh
VMCAI 2004: 252-266
[pdf]
On the
Expressive Power of Canonical Abstraction
Shmuel Sagiv
VMCAI 2004: 58
[pdf]
Interprocedural
functional shape analysis using local heaps
Noam Rinetzky,Shmuel Sagiv, and Eran Yahav
TR-26/04
[pdf]
2003
Verifying
Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
ESOP 2003: 204-222
[pdf]
Verifying
Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
ESOP 2003: 204-222
[pdf]
Finite
Differencing of Logical Formulas for Static Analysis
Thomas W. Reps, Shmuel Sagiv, Alexey Loginov
ESOP 2003: 380-398
[pdf]
CSSV: towards a
realistic tool for statically detecting all buffer overflows in C
Nurit Dor, Michael Rodeh, Shmuel Sagiv
PLDI 2003: 155-167
[pdf]
Establishing
Local Temporal Heap Safety Properties with Applications to Compile-Time Memory
Management
Ran Shaham, Eran Yahav, Elliot K. Kolodner, Shmuel Sagiv
SAS 2003: 483-503
[pdf]
Logical
Characterizations of Heap Abstractions
Greta Yorsh, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
CoRR cs.LO/0312014: (2003)
[pdf]
Automatically
Verifying Concurrent Queue Algorithms
Eran Yahav, Shmuel Sagiv
Electr. Notes Theor. Comput. Sci. 89(3): (2003)
[pdf]
shape Analysis
and applications
Thomas W. Reps, Reinhard Wilhelm, Mooly Sagiv
CRC press (2003), 175-217
[pdf]
2002
Online Subpath
Profiling
David Oren, Yossi Matias, Shmuel Sagiv
CC 2002: 78-94
[pdf]
Semantic
Minimization of 3-Valued Propositional Formulae
Thomas W. Reps, Alexey Loginov, Shmuel Sagiv
LICS 2002: 40 -
[pdf]
Estimating the
impact of heap liveness information on space consumption in Java
Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv
MSP/ISMM 2002: 171-182
[pdf]
Deriving
Specialized Program Analyses for Certifying Component-Client Conformance
G. Ramalingam, Alex Varshavsky, John Field, Deepak Goyal, Shmuel Sagiv
PLDI 2002: 83-94
[pdf]
Compactly
Representing First-Order Structures for Static Analysis
Roman Manevich, G. Ramalingam, John Field, Deepak Goyal, Shmuel Sagiv
SAS 2002: 196-212
[pdf]
Shape Analysis
and Applications
Reinhard Wilhelm, Thomas W. Reps, Shmuel Sagiv
The Compiler Design Handbook 2002: 175-218
[pdf]
Parametric
shape analysis via 3-valued logic
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm
ACM Trans. Program. Lang. Syst. 24(3): 217-298 (2002)
[pdf]
2001
Interprocedural
Shape Analysis for Recursive Programs
Noam Rinetzky, Shmuel Sagiv
CC 2001: 133-149
[pdf]
Heap Profiling
for Space-Efficient Java
Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv
PLDI 2001: 104-113
[pdf]
Cleanness
Checking of String Manipulations in C Programs via Integer Analysis
Nurit Dor, Michael Rodeh, Shmuel Sagiv
SAS 2001: 194-212
[pdf]
Kleene's Logic
with Equality
Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv
Inf. Process. Lett. 80(3): 131-137 (2001)
[pdf]
2000
Shape Analysis
Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps
CC 2000: 1-17
[pdf]
Automatic
Removal of Array Memory Leaks in Java
Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv
CC 2000: 50-66
[pdf]
A Kleene
Analysis of Mobile Ambients
Flemming Nielson, Hanne Riis Nielson, Shmuel Sagiv
ESOP 2000: 305-319
[pdf]
On the
Effectiveness of GC in Java
Ran Shaham, Elliot K. Kolodner, Shmuel Sagiv
ISMM 2000: 12-17
[pdf]
Putting static
analysis to work for verification: A case study
Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
ISSTA 2000: 26-38
[pdf]
Checking
Cleanness in Linked Lists
Nurit Dor, Michael Rodeh, Shmuel Sagiv
SAS 2000: 115-134
[pdf]
TVLA: A System
for Implementing Static Analyses
Tal Lev-Ami, Shmuel Sagiv
SAS 2000: 280-301
[pdf]
1999
A Decidable
Logic for Describing Linked Data Structures
Michael Benedikt, Thomas W. Reps, Shmuel Sagiv
ESOP 1999: 2-19
[pdf]
Parametric
Shape Analysis via 3-Valued Logic
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm
POPL 1999: 105-118
[pdf]
Finding
Circular Attributes in Attribute Grammars
Michael Rodeh, Shmuel Sagiv
J. ACM 46(4): 556 (1999)
[pdf]
1998
Building a
Bridge between Pointer Aliases and Program Dependences
John L. Ross, Shmuel Sagiv
ESOP 1998: 221-235
[pdf]
Detecting
Memory Errors via Static Pointer Analysis (Preliminary Experience)
Nurit Dor, Michael Rodeh, Shmuel Sagiv
PASTE 1998: 27-34
[pdf]
Edge Profiling
versus Path Profiling: The Showdown
Thomas Ball, Peter Mataga, Shmuel Sagiv
POPL 1998: 134-148
[pdf]
Solving
Shape-Analysis Problems in Languages with Destructive Updating
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm
ACM Trans. Program. Lang. Syst. 20(1): 1-50 (1998)
[pdf]
A Logic-Based
Approach to Program Flow Analysis
Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm
Acta Inf. 35(6): 457-504 (1998)
[pdf]
Parametric
shape analysis via 3-valued logic
Sagiv M., Reps T., Wilhelm R.
TR-1383, Computer sciences department, University of Wisconsin, Madison,
WI,August 1998
[pdf]
1996
Solving Shape-Analysis
Problems in Languages with Destructive Updating
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm
POPL 1996: 16-31
[pdf]
Precise Interprocedural
Dataflow Analysis with Applications to Constant Propagation
Shmuel Sagiv, Thomas W. Reps, Susan Horwitz
Theor. Comput. Sci. 167(1&2): 131-170 (1996)
[pdf]
1995
Precise
Interprocedural Dataflow Analysis via Graph Reachability
Thomas W. Reps, Susan Horwitz, Shmuel Sagiv
POPL 1995: 49-61
[pdf]
Demand
Interprocedural Dataflow Analysis
Susan Horwitz, Thomas W. Reps, Shmuel Sagiv
SIGSOFT FSE 1995: 104-115
[pdf]
Precise
Interprocedural Dataflow Analysis with Applications to Constant Propagation
Shmuel Sagiv, Thomas W. Reps, Susan Horwitz
TAPSOFT 1995: 651-665
[pdf]
1994
Speeding up
Slicing
Thomas W. Reps, Susan Horwitz, Genevieve Rosay, Molly Sagiv
SIGSOFT FSE 1994: 11-20
[pdf]
1993
Walleye: A tool
for PL/MP migration: Technical issues
Mooly Sagiv, Nelson L., Richard G.
IBM Israel scientific center, TR 88-343
[pdf]
1992
Proving Safety
of Speculative Load Instructions at Compile Time
David Bernstein, Michael Rodeh, Shmuel Sagiv
ESOP 1992: 56-72
[pdf]
The Expressive
Power of Side Effects in Prolog
Johann A. Makowsky, J.-C. Gregoire, Shmuel Sagiv
J. Log. Program. 12(1&2): 179-188 (1992)
[pdf]
1990
A Logic-Based
Approach to Data Flow Analysis Problem
Shmuel Sagiv, Nissim Francez, Michael Rodeh, Reinhard Wilhelm
PLILP 1990: 277-292
[pdf]
Analyzing
interprocedural aliases through pointer equalities
Mooly Sagiv, Rodeh M.
IBM Israel scientific center, technical repport 88.298 (December 1990)
[pdf]
1989
Resolving
Circularity in Attribute Grammars with Applications to Data Flow Analysis
Shmuel Sagiv, O. Edelstein, Nissim Francez, Michael Rodeh
POPL 1989: 36-48
[pdf]
1986
Machine
independent optimizations via attribute grammars
Edelstein O.,Mooly Sagiv
IBM Israel scientific center, technical repport 88.187 (June 1986)
[pdf]