Presentations/Talks
- OCamlFDO: Feedback-Directed Optimization for OCaml [Slides]
- Unbounded Superoptimization [Slides]
- How to generate efficient code for new hardware?
- Abstraction-guided synthesis. [Slides]
- Concurrency seminar, Oxford University Computing Laboratory, UK, December 2009.
- Formal Methods Seminar, Hebrew University, Jerusalem, January 2010.
- Programming Languages Seminar, State University of New York at Stony Brook, April 2010.
- Programming Languages and Systems Group Seminar, Imperial College London, August 2012.
- Shape analysis overview.
[Slides]
Presented in Dagstuhl Seminar on
Typing, Analysis and Verification of Heap-Manipulating Programs
, July 2009.
- Phalanx: Parallel Checking of Expressive Heap Assertions.
[Slides]
Presented in Dagstuhl Seminar on
Typing, Analysis and Verification of Heap-Manipulating Programs
, July 2009.
- Inferring Synchronization under Limited Observability.
[Slides]
- Dagstuhl seminar on Software Synthesis, December 2009.
- PL&SE Seminar, IBM T.J. Watson Research Center, Hawthorne, October 2008.
- Formal Methods Seminar, Hebrew University, Jerusalem, July 2008.
- Programming Languages Seminar, Tel Aviv University, July 2008.
- Tutorial: Introduction to Separation Logic.
[Slides]
Presented in Concurrency Reading Group,
IBM T.J. Watson Research Center, Hawthorne, April 2008.
- A Logic of Reachable Patterns in Linked Data-Structures.
[Slides].
- Conference talk at
FOSSACS
2006.
- Invited talk at HAV workshop, March 2007.
- Computer Laboratory
Logic and Semantics Seminar, University of Cambridge, UK, February
2007.
- Research
Seminar, Analysis of computer systems (ACSys) group, NYU, October
2007.
- Seminar
in Computational Logic, CUNY,
September, 2007.
-
Semantics and its
Applications Workshop, CS-TAU, December 2005.
-
Dagstuhl seminar "Software Verification:
Infinite-State Model Checking and Static Program Analysis",
February 2006.
-
A Combination Method for
Generating Interpolants. [Slides]
-
Abstraction for Falsification.
[Slides]
- Conference talk at
CAV
2005.
-
Also presentated at MSR Cambridge, June 2005.
-
Symbolically computing most-precise abstract operations for shape analysis.
[Slides]
-
Symbolic implementation of the best transformer. [Slides]
-
Logical characterizations of heap abstractions.