People

Mooly Sagiv

PhD.: High Level Formalisms for Program Flow Analysis and their use in Compiling [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~msagiv/

Tal Lev-Ami

MsC.: TVLA: A Framework for Kleene Logic Based Static Analyses  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~tla

Ohad Shacham

MsC.:  Scaling Model Checking of Dataraces Using Dynamic Information  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~ohads

Nurit Dor

PhD.: Automatic Verification of Program Cleanness  [pdf] [Bibtex]
MsC.: Detecting Memory Errors via Static Pointer Analysis  [pdf] [Bibtex]

Home page: http://nurit.dor.googlepages.com/

Roman Manevich

PhD.: Partially Disjunctive Shape Analysis (submitted) [pdf] [Bibtex]
MsC.: Data Structures and Algorithms for Efficient Shape Analysis  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~rumster/

Noam Rinetzky

PhD.: Interprocedural and modular local heap shape analysis  [pdf] [Bibtex]
MsC.: Interprocedural shape analysis  [pdf] [Bibtex]

Home page: http://www.dcs.qmul.ac.uk/~maon/

Ran Shacham

PhD.: Heap Liveness Based Memory Management: Potentials, Tools, and Algorithms  [pdf] [Bibtex]
MsC.: Automatic Removal of Array Memory leaks in Java  [pdf] [Bibtex]

Home page: 

Eran Yahav

PhD.: Property-Guided Verification of Concurrent Heap-Manipulating Programs  [pdf] [Bibtex]

Home page: http://www.research.ibm.com/people/e/eyahav/

Greta Yorsh

PhD.: Employing decision procedures for verification of heap-manipulating programs.  [pdf] [Bibtex]
MsC.: Logical Characterizations of Heap Abstractions  [pdf] [Bibtex]

Home page: http://www.research.ibm.com/people/g/gretay/index.html

Shachar Itzhaky

Aharon Abadi

Daphna Amit

MsC.: Comparison under Abstraction for Verifying Linearizability  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~amitdaph/

Gilad Arnold

MsC.:  Combining Heap Analyses by Intersecting Abstractions  [pdf] [Bibtex]

Home page: http://www.cs.berkeley.edu/~arnold

Ron Ellenbogen

MsC.:  Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis  [pdf] [Bibtex]

Guy Erez

MsC.: Generating Concrete Counterexamples for Sound Abstract Interpretations  [pdf] [Bibtex]

Guy Gueta

Uri Juhasz

MsC.: Modular Verification with Shared Abstractions  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~urijuhasz

Shay Litvak

Ronny Morad

David Oren

MsC.: Online Subpath Profiling  [pdf] [Bibtex]

Michael Pan

MsC.: HUP: A Heap Usage Profiling Tool for Java Programs  [pdf] [Bibtex]

Tool page: http://hup.sourceforge.net/

Shachar Rubunstein

MsC.:  On the utility of cutpoints for monitoring program execution  [pdf] [Bibtex]

Yair Sade

MsC.:  Optimizing C Multithreaded Memory Management using Thread-Local Storage  [pdf] [Bibtex]

Michal Segalov

MsC.: Efficiently Inferring Thread Correlations  [pdf] [Bibtex]

Home page: http://www.cs.tau.ac.il/~segalovm

Alex Varshavsky

MsC.: Deriving Specialized Heap Analyses for Verifying Component-Client Conformance  [ps] [Bibtex]

Home page: http://www.cs.toronto.edu/~walex