INVITED TALKS

• The Bugs that went to Mars and Terrorized Earth
  Keynote, International Symposium on Software Reliability Engineering (ISSRE), Ottawa, Canada Oct 2016
• Managing data for Curiosity, fun and profit
  NASA Formal Methods Conference, Mountain View, CA, May 2013
• Verifying a flash filesystem
  Microsoft Software Summit, Paris, France, Apr 2011
• Programming With Miracles
  Industrial Formal Methods, Nancy, France, Oct 2010
• Opportunistic Formal Methods
  European Space Agency Formal Methods in Software Engineering Workshop (FMSE), Noordwijk, The Netherlands, Nov 2009
• Analyzing telemetry logs
  Workshop on Verified Software: Theory, Tools, and Experiments, Eindhoven, The Netherlands, Nov 2009
  
• Analyzing telemetry logs
  IFIP WG 2.3 Meeting, Boston, MA, Jun 2009
• "Non Local" Commutativity
  IFIP WG 2.3 Meeting, Cambridge, U.K., Jul 2008
• Specifying Filesystems Robust to Hardware Failures
  IFIP WG 2.3 Meeting, Santa Fe, Oct 2007
• Improving Software Reliability With Formal Verification Tools
  Guest lecturer and panelist at NASA NESC Academy course on Software Engineering, Fairfax, VA, Mar 2007
• Towards Reliable Software
  Caltech Connections Workshop, Pasadena, CA, Jul 2007
• Reliable Software Systems Development Project
  JPL/Goddard Quality Management Software Workshop, May 2005
• Verifun: A Theorem Prover Using Lazy Proof Explication
  Stanford Summer School on Combination of Decision Procedures, SRI, Aug 2004
• Static Source Code Analysis for Software Verification
  JPL Software Test Guild Symposium, Pasadena, Jun 2004
• Verifun: A Theorem Prover based on Proof Explication
  Microsoft Research Symposium, Redmond, Aug 2003
• Verifun: A Theorem Prover based on Proof Explication
  SRI International, Jul 2003
• Verifun: An Explicating Theorem Prover
  Oregon Graduate Institute, Nov 2002
• Denali: A goal-directed superoptimizer
  Ludwig-Maximilians-Universitaet, Munich, Jun 2002
• Denali: A goal-directed superoptimizer
  University of California at Berkeley, Berkeley, Mar 2002
• Denali: A goal-directed superoptimizer
  University of Texas at Austin, May 2001
• Annotation Inference for Modular Checkers
  Caltech Brown Bag Seminar, Pasadena, Oct 2000
• A Semantic Approach to Secure Information Flow
  Technische Universitaet Munich (TU-Munich), May 2000
• Invited panel presentation
  E. W. Dijkstra Retirement Symposium, Austin, May 2000