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/

 

Current PhD. Students

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

 

Past PhD. Students

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

 

Current MsC. Students

Shachar Itzhaky

 

Past MsC. Students

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