Recent Presentations/Talks

• Unbounded Superoptimization [Slides]
  • Workshop on Formal Methods and Tools for Security (FMATS5), Cambridge, UK, September 2017.
• How to generate efficient code for new hardware?
  • MICRO Career Workshop for Women and Minorities in Computer Architecture, Cambridge, UK, December 2014.
• 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]
  • Conference talk at CADE-20, 2005.
• 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]
  • Conference talk at TACAS 2004.
  • Dagstuhl seminar "Applied Deductive Verification" . November 2003. [Slides]
• Symbolic implementation of the best transformer. [Slides]
  • Conference talk at VMCAI 2004.
• Logical characterizations of heap abstractions.
  • Logic seminar at CS-TAU, March 2003. [Slides]
  • Dagstuhl seminar "Reasoning about shape", March 2003. [Slides]