Person: Shmuel Sagiv

DBLP: Sagiv:Shmuel

Facilitated 1 volumes:

Ed

Contributed to:

2008

2006

2005

2005

2005

2005

2005

2004

2004

2004

2004

2004

2003

2003

2003

2002

2002

2002

2002

2002

2001

2001

2001

2000

2000

2000

2000

2000

1999

1999

1998

1998

1998

1996

1995

1995

1994

1992

1990

1989

1995

1996

Wrote 50 papers:

CAV-2008-BerdineLMRS #analysis #concurrent #quantifier #thread

Thread Quantification for Concurrent Shape Analysis (JB, TLA, RM, GR, SS), pp. 399–413.

CAV-2006-Lev-AmiIS #abstraction #analysis #performance #precise

Abstraction for Shape Analysis with Fast and Precise Transformers (TLA, NI, SS), pp. 547–561.

CADE-2005-Lev-AmiIRSSY #data type #first-order #linked data #logic #open data #reachability #simulation #using #verification

Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures (TLA, NI, TWR, SS, SS, GY), pp. 99–115.

CAV-2005-LoginovRS #abstraction #induction #learning #refinement

Abstraction Refinement via Inductive Learning (AL, TWR, SS), pp. 519–533.

CC-2005-SadeSS #c #memory management #optimisation #parallel #thread #using

Optimizing C Multithreaded Memory Management Using Thread-Local Storage (YS, SS, RS), pp. 137–155.

POPL-2005-GopanRS #analysis #array #framework

A framework for numeric analysis of array operations (DG, TWR, SS), pp. 338–350.

POPL-2005-RinetzkyBRSW #abstraction #semantics

A semantics for procedure local heaps and its abstractions (NR, JB, TWR, SS, RW), pp. 296–309.

VMCAI-2005-ManevichYRS #abstraction #canonical

Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists (RM, EY, GR, SS), pp. 181–198.

CAV-2004-ImmermanRRSY #simulation #verification

Verification via Structure Simulation (NI, AMR, TWR, SS, GY), pp. 281–294.

CAV-2004-RepsSW #logic #program analysis

Static Program Analysis via 3-Valued Logic (TWR, SS, RW), pp. 15–30.

CSL-2004-ImmermanRRSY #bound #decidability #logic #transitive

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics (NI, AMR, TWR, SS, GY), pp. 160–174.

SAS-2004-JeannetLRS #analysis #approach #interprocedural #relational

A Relational Approach to Interprocedural Shape Analysis (BJ, AL, TWR, SS), pp. 246–264.

SAS-2004-ManevichSRF #abstraction

Partially Disjunctive Heap Abstraction (RM, SS, GR, JF), pp. 265–279.

TACAS-2004-GopanDDRS

Numeric Domains with Summarized Dimensions (DG, FD, ND, TWR, SS), pp. 512–529.

TACAS-2004-YorshRS #analysis

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis (GY, TWR, SS), pp. 530–545.

VMCAI-2004-RepsSY #implementation

Symbolic Implementation of the Best Transformer (TWR, SS, GY), pp. 252–266.

VMCAI-2004-Sagiv #abstraction #canonical #on the #power of

On the Expressive Power of Canonical Abstraction (SS), p. 58.

ESOP-2003-RepsSL #difference #finite #logic #static analysis

Finite Differencing of Logical Formulas for Static Analysis (TWR, SS, AL), pp. 380–398.

ESOP-2003-YahavRSW #evolution #logic #verification

Verifying Temporal Heap Properties Specified via Evolution Logic (EY, TWR, SS, RW), pp. 204–222.

PLDI-2003-DorRS #c #detection #named #towards

CSSV: towards a realistic tool for statically detecting all buffer overflows in C (ND, MR, SS), pp. 155–167.

SAS-2003-ShahamYKS #memory management #safety

Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management (RS, EY, EKK, SS), pp. 483–503.

CC-2002-OrenMS #online #profiling

Online Subpath Profiling (DO, YM, SS), pp. 78–94.

ISMM-2002-ShahamKS #impact analysis #java #liveness

Estimating the impact of heap liveness information on space consumption in Java (RS, EKK, SS), pp. 171–182.

LICS-2002-RepsLS #semantics

Semantic Minimization of 3-Valued Propositional Formulae (TWR, AL, SS), p. 40–?.

PLDI-2002-RamalingamWFGS #analysis #component #consistency

Deriving Specialized Program Analyses for Certifying Component-Client Conformance (GR, AV, JF, DG, SS), pp. 83–94.

SAS-2002-ManevichRFGS #first-order #representation #static analysis

Compactly Representing First-Order Structures for Static Analysis (RM, GR, JF, DG, SS), pp. 196–212.

CC-2001-RinetzkyS #analysis #interprocedural #recursion #source code

Interprocedural Shape Analysis for Recursive Programs (NR, SS), pp. 133–149.

PLDI-2001-ShahamKS #java #profiling

Heap Profiling for Space-Efficient Java (RS, EKK, SS), pp. 104–113.

SAS-2001-DorRS #analysis #c #integer #source code #string

Cleanness Checking of String Manipulations in C Programs via Integer Analysis (ND, MR, SS), pp. 194–212.

CC-2000-ShahamKS #array #automation #java #memory management

Automatic Removal of Array Memory Leaks in Java (RS, EKK, SS), pp. 50–66.

CC-2000-WilhelmSR #analysis

Shape Analysis (RW, SS, TWR), pp. 1–17.

ESOP-2000-NielsonNS #analysis #mobile

A Kleene Analysis of Mobile Ambients (FN, HRN, SS), pp. 305–319.

ISMM-2000-ShahamKS #effectiveness #garbage collection #java #on the

On the Effectiveness of GC in Java (RS, EKK, SS), pp. 12–17.

ISSTA-2000-Lev-AmiRSW #case study #static analysis #verification

Putting static analysis to work for verification: A case study (TLA, TWR, SS, RW), pp. 26–38.

SAS-2000-DorRS

Checking Cleanness in Linked Lists (ND, MR, SS), pp. 115–134.

SAS-2000-Lev-AmiS #analysis #implementation #named

TVLA: A System for Implementing Static Analyses (TLA, SS), pp. 280–301.

ESOP-1999-BenediktRS #data type #decidability #linked data #logic #open data

A Decidable Logic for Describing Linked Data Structures (MB, TWR, SS), pp. 2–19.

POPL-1999-SagivRW #analysis #logic #parametricity

Parametric Shape Analysis via 3-Valued Logic (SS, TWR, RW), pp. 105–118.

ESOP-1998-RossS #alias #dependence #pointer

Building a Bridge between Pointer Aliases and Program Dependences (JLR, SS), pp. 221–235.

PASTE-1998-DorRS #analysis #detection #experience #fault #memory management #pointer

Detecting Memory Errors via Static Pointer Analysis (Preliminary Experience) (ND, MR, SS), pp. 27–34.

POPL-1998-BallMS #profiling

Edge Profiling versus Path Profiling: The Showdown (TB, PM, SS), pp. 134–148.

POPL-1996-SagivRW #problem

Solving Shape-Analysis Problems in Languages with Destructive Updating (SS, TWR, RW), pp. 16–31.

FSE-1995-HorwitzRS #analysis #data flow #interprocedural

Demand Interprocedural Dataflow Analysis (SH, TWR, SS), pp. 104–115.

POPL-1995-RepsHS #analysis #data flow #graph #interprocedural #precise #reachability

Precise Interprocedural Dataflow Analysis via Graph Reachability (TWR, SH, SS), pp. 49–61.

FSE-1994-RepsHSR #slicing

Speeding up Slicing (TWR, SH, SS, GR), pp. 11–20.

ESOP-1992-BernsteinRS #proving #safety

Proving Safety of Speculative Load Instructions at Compile Time (DB, MR, SS), pp. 56–72.

PLILP-1990-SagivFRW #analysis #approach #data flow #problem

A Logic-Based Approach to Data Flow Analysis Problem (SS, NF, MR, RW), pp. 277–292.

POPL-1989-SagivEFR #analysis #attribute grammar #data flow

Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis (SS, OE, NF, MR), pp. 36–48.

TAPSOFT-1995-SagivRH #analysis #constant #data flow #interprocedural #precise

Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation (SS, TWR, SH), pp. 651–665.

TAPSOFT-J-1995-SagivRH96 #analysis #constant #data flow #interprocedural #precise

Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation (SS, TWR, SH), pp. 131–170.