Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Sagiv's Selected Publications
Sagiv's Selected Publications
Shape and Pointer and Heap Analysis
Shaham, R., Yahav, Kolodner, E., and Sagiv M.:
Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management.
To Appear in the Science of Computer Programming Journal.
An earlier version appeared in
in the 10th International Static Analysis Symposium (SAS '03)
Rinetzky N., Sagiv M., and Yahav E.:
Interprocedural functional shape analysis using local heaps.
in TR-26/04, School of Computer Science, Tel Aviv University, November 2004
Rinetzky N., Bauer J. Reps T., Sagiv M., and Wilhelm R.:
A semantics for procedure local heaps
and its abstraction.
In the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005
Manevich R., Sagiv, M., Ramalingam G., and Field J.:
Partially Disjunctive Heap Abstraction
in the 11th International Static Analysis Symposium (SAS '04)
Jeannet, B., Loginov, A., Reps, T., and Sagiv, M.:
A relational approach to interprocedural shape analysis.
in the 11th International Static Analysis Symposium (SAS '04)
Yorsh, G., Reps, T., and Sagiv, M.:
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. Yahav E. and Sagiv M.:
Automatically Verifying Concurrent Queue
Algorithms.
In SoftMC 2003
Yahav, E., Reps, T., Sagiv, S., Wilhelm, R.:
Verifying Temporal Heap Properties Specified via Evolution Logic.
in European Symposium on Programming (ESOP 2003): 204-222
Reps, T., Sagiv, S., and Loginov, A.:
Finite Differencing of Logical Formulas
for Static Analysis.
in European Symposium on Programming (ESOP 2003): 380-398
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv M.:
Deriving Specialized Program Analyses for
Certifying Component-Client Conformance.
PLDI 2002: 83-94
Manevich, R., Ramalingam, G., Field J,, Goyal, D., Sagiv, M.:
Compactly Representing First-Order Structures
for Static Analysis .
SAS 2002: 196-212
Sagiv M., Reps T, and Wilhelm R.:
Parametric shape analysis via 3-valued
logic
TOPLAS, 24:3 (2002)
An earlier version appeared in The 26th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL'99)
Rinetskey N., and Sagiv M.:
Interprocedural Shape Analysis for Recursive
Programs
in International Conference on Compiler Construction(CC'01)
Lev-Ami, T., Reps, T., Sagiv, M.: and Wilhelm, R.:
Putting Static Analysis to Work for Verification: A Case Study
in ISSTA 2000 (August 2000)
Dor, N., Rodeh, M., and Sagiv, M.:
Checking Cleanness in Linked Lists.
in Seventh International Static Analysis Symposium (SAS'00)
Lev-Ami, T. and Sagiv, M.:
TVLA: A System for Implementing Static Analyses
in Seventh International Static Analysis Symposium (SAS'00)
Ross, J. and Sagiv, M.:
Building a Bridge between Pointer Aliases
and Program Dependences.
In Nordic Journal of Computing (8)1998, 361-386
An earlier version appeared in ESOP'98
Sagiv, M., Reps, T., and Wilhelm, R.:
Solving shape-analysis problems in languages with destructive updating.
in TOPLAS, 20:1 (January 1998), 1-50.
Decision Procedures for Linked Data Structures
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh., G.:
The Boundary Between Decidability and
Undecidability for Transitive-Closure Logics
n CSL'04, Annual conference of the European Conference on Computer Science Logic
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh., G.:
Verification Via Structure Simulation
n CAV'04 16th International Conference on Computer Aided Verification
Benedikt, M., Reps, T., and Sagiv, M.:
A Decidable Logic for Describing Linked Data Structures.
In European Symposium On Programming (Amsterdam 22-26 March 1999)
3-Valued Logics
Reps, T., Loginov, A., Sagiv S.:
Semantic Minimization of 3-Valued Propositional Formulae.
in LICS 2002
String Analysis
Dor, N., Rodeh, M., and Sagiv M.: CSSV:
Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C.
In ACM SIGPLAN 2003 Conference on
Programming Language Design and Implementation (PLDI'03)
Dor, N., Rodeh, M., and Sagiv, M.:
Cleanness Checking of String Manipulations in C
Programs via Integer Analysis.
in Eighth International Static Analysis Symposium (SAS'01)
Abstract Interpretation
Gopan D., Reps T., and Sagiv M.:
A Framework for Numeric Analysis of Array Operations.
In the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005
Gopan, D., DiMaio F., Dor, N., Reps T., and Sagiv., M.:
Numeric Domains with Summarized Dimensions.
In TACAS 2004: 512-529
Reps, T., Sagiv, M., and Yorsh, G.:
Symbolic Implementation of the Best Transformer.
In VMCAI 2004: 252-266
Shaham, R., Kolodner E., and Sagiv, M.:
Automatic removal of array memory leaks in Java
In 9th International Conference on Compiler Construction (CC'00)
Nielson F., Nielson H.R., and Sagiv M.:
Kleene's Logic with Equality.
in Information Processing Letters Volume 80, Number 3, 15 November 2001, 131-137
Nielson, F. Ries Nielson, H., and Sagiv M.:
A Kleene analysis of mobile ambients
In European Symposium On Programming(Berlin, 27 March - 2 April 2000)
Memory Management
Sade Y., Sagiv M. and Shaham R.:
Optimizing C Multithreaded Memory Management Using Thread-Local Storage
In 14th International Conference on Compiler Construction (CC'05), 2005
Shaham R., Kolodner E., and Sagiv M.:
Estimating the Impact of Heap Liveness Information on Space Consumption in Java.
In The 2002 International Symposium on Memory Management (ISMM '02) Berlin, Germany, June 2002.
Shaham, R., Kolodner, E., and Sagiv M.:
Heap Profiling for Space-Efficient Java
in ACM SIGPLAN 2001 Conference on
Programming Language Design and Implementation (PLDI'01)
Shaham ,R., Kolodner, E.,, and Sagiv, M.:
On the Effectiveness of GC in Java.
in The 2000 International Symposium on Memory Management (ISMM '00) Minneapolis, Minnesota, USA, October 2000.
Path Profiling
Oren, D., Matias, Y., and Sagiv, S: Online Subpath Profiling.
in Compiler Construction, 11th International Conference (CC 2002): 78-94