Mooly SagivPhD.: 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-AmiMsC.: TVLA: A Framework for Kleene Logic Based Static Analyses [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~tla |
|
Ohad ShachamMsC.: Scaling Model Checking of Dataraces Using Dynamic Information [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~ohads |
|
Past PhD. Students
Nurit DorPhD.: Automatic Verification of Program Cleanness [pdf] [Bibtex] Home page: http://nurit.dor.googlepages.com/ |
|
Roman ManevichPhD.: Partially Disjunctive Shape Analysis (submitted) [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~rumster/ |
|
Noam RinetzkyPhD.: Interprocedural and modular local heap shape analysis [pdf] [Bibtex] Home page: http://www.dcs.qmul.ac.uk/~maon/ |
|
Ran ShachamPhD.: Heap Liveness Based Memory Management: Potentials, Tools, and Algorithms [pdf] [Bibtex] |
|
Eran YahavPhD.: Property-Guided Verification of Concurrent Heap-Manipulating Programs [pdf] [Bibtex] Home page: http://www.research.ibm.com/people/e/eyahav/ |
|
Greta YorshPhD.: Employing decision procedures for verification of heap-manipulating programs. [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 AmitMsC.: Comparison under Abstraction for Verifying Linearizability [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~amitdaph/ |
|
Gilad ArnoldMsC.: Combining Heap Analyses by Intersecting Abstractions [pdf] [Bibtex] Home page: http://www.cs.berkeley.edu/~arnold |
|
Ron EllenbogenMsC.: Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis [pdf] [Bibtex] |
|
Guy ErezMsC.: Generating Concrete Counterexamples for Sound Abstract Interpretations [pdf] [Bibtex] |
|
Guy Gueta |
|
Uri JuhaszMsC.: Modular Verification with Shared Abstractions [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~urijuhasz |
|
Shay Litvak |
|
Ronny Morad |
|
David Oren |
|
Michael PanMsC.: HUP: A Heap Usage Profiling Tool for Java Programs [pdf] [Bibtex] Tool page: http://hup.sourceforge.net/ |
|
Shachar RubunsteinMsC.: On the utility of cutpoints for monitoring program execution [pdf] [Bibtex] |
|
Yair SadeMsC.: Optimizing C Multithreaded Memory Management using Thread-Local Storage [pdf] [Bibtex] |
|
Michal SegalovMsC.: Efficiently Inferring Thread Correlations [pdf] [Bibtex] Home page: http://www.cs.tau.ac.il/~segalovm |
|
Alex VarshavskyMsC.: Deriving Specialized Heap Analyses for Verifying Component-Client Conformance [ps] [Bibtex] Home page: http://www.cs.toronto.edu/~walex |
|