Recent Presentations/Talks
 How to generate efficient code for new hardware?
 Abstractionguided 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 HeapManipulating Programs
, July 2009.
 Phalanx: Parallel Checking of Expressive Heap Assertions.
[Slides]
Presented in Dagstuhl Seminar on
Typing, Analysis and Verification of HeapManipulating 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 DataStructures.
[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, CSTAU, December 2005.

Dagstuhl seminar "Software Verification:
InfiniteState 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 mostprecise abstract operations for shape analysis.
[Slides]

Symbolic implementation of the best transformer. [Slides]

Logical characterizations of heap abstractions.