June 10, 2011
The Flow-Insensitive Precision of Andersen's Analysis in Practice
University of California, Berkeley
March 16, 2011
Xisa: Extensible Inductive Shape Analysis
Carnegie Mellon University
February 25, 2011
Programming Languages Research Overview
University of Colorado, Boulder
Prospective Ph.D. Student Open House
December 17, 2010
Calling Context Abstraction with Shapes
National Taiwan University
March 6, 2010
Programming Languages Research Overview
University of Colorado, Boulder
Prospective Ph.D. Student Open House
December 5, 2009
Mixing Type Checking and Symbolic Execution
FRACTAL F2009: Front Range Architecture Compilers Tools and Languages Workshop
Boulder, Colorado, USA
August 11, 2009
End-User Shape Analysis
National Taiwan University
August 11, 2009
Using Checkers for End-User Shape Analysis
National Taiwan University
July 24, 2009
Reduction in End-User Shape Analysis
Dagstuhl Seminar 09301: Typing, Analysis, and Verification of Heap-Manipulating Programs
June 16, 2009
Gradual Programming: Bridging the Semantic Gap
PLDI-FIT 2009: Fun Ideas and Thoughts at PLDI
Dublin, Ireland
November 24, 2008
End-User Program Analysis for Data Structures
University of Virginia
August 28, 2008
End-User Program Analysis
University of California, Berkeley
Dissertation Talk
May 16, 2008
Extensible Shape Analysis by Designing with the User in Mind
OSQ 2008: Open Source Quality Project Retreat
Santa Cruz, California, USA
Spring 2008
Precise Program Analysis with Data Structures
Job Talk
January 11, 2008
Relational Inductive Shape Analysis
POPL 2008: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
San Francisco, California, USA
August 27, 2007
Materialization in Shape Analysis with Structural Invariant Checkers
IT University of Copenhagen
August 24, 2007
Shape Analysis with Structural Invariant Checkers
SAS 2007: International Static Analysis Symposium
May 10, 2007
Shape Analysis with Structural Invariant Checkers
OSQ 2006: Open Source Quality Project Retreat
Santa Cruz, California, USA
August 31, 2006
Analysis of Low-Level Code Using Cooperating Decompilers
SAS 2006: International Static Analysis Symposium
May 12, 2005
Compositional Verifiers for Mobile Code Safety
OSQ 2005: Open Source Quality Project Retreat
Santa Cruz, California, USA
"5-minute madness"
May 5, 2005
Proof-Carrying Verifiers: Sound and Efficient Mobile Code Verification
With Adam Chlipala
Fourth Annual Berkeley-Stanford Computer Science Day
Stanford University
January 21, 2005
Inferring Object Invariants
AIOOL 2005: International Workshop on Abstract Interpretation of Object-Oriented Languages
January 18, 2005
Abstract Interpretation with Alien Expressions and Heap Structures
VMCAI 2005: International Conference on Verification, Model Checking, and Abstract Interpretation
January 10, 2005
Type-Based Verification of Assembly Language for Compiler Debugging
TLDI 2005: ACM SIGPLAN International Workshop on Types in Language Design and Implementation
November 12, 2004
Abstract Interpretation with Alien Expressions and Heap Structures
Open Source Quality Project Meeting
University of California, Berkeley
May 13, 2004
Extensible Verification of Untrusted Code
OSQ 2004: Open Source Quality Project Retreat
Santa Cruz, California, USA
May 13, 2004 2004
Coolaid: Debugging Compilers with Verification
OSQ 2004: Open Source Quality Project Retreat
Santa Cruz, California, USA
"5-minute madness"
November 11, 2003
Programming Languages for Biology
Open Source Quality Project Meeting
University of California, Berkeley
October 21, 2003
Under the Hood of the Open Verifier
Open Source Quality Project Meeting
University of California, Berkeley
September 6, 2003
PML: Toward a High-Level Formal Language for Biological Systems
BioConcur 2003: Workshop on Concurrent Models in Molecular Biology
July 24, 2003
PML: Toward a High-Level Formal Language for Biological Systems
Computational Biology Research Group Meeting
University of California, Berkeley
May 13, 2003
Coolaid: Debugging Compilers with Untrusted Code Verification
OSQ 2003: Open Source Quality Project Retreat
Santa Cruz, California, USA
"5-minute madness"
May 8, 2002
Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective
Senior Research Thesis - Final Presentation Meeting of the Minds (think Out LOUD) - Undergraduate Research Symposium Carnegie Mellon University
March 20, 2002
Towards Programming in a Certified Computing Framework
Senior Research Thesis - Mid-Semester Presentation Carnegie Mellon University
February 19, 2002; February 26, 2002
Realizing ConCert
With Tom Murphy, Margaret DeLap, and Jason Liszka ConCert Project Meeting Carnegie Mellon University
December 12, 2001
An Application for a Certified Grid Computing Framework: Parallel Theorem Proving for Linear Logic
Senior Research Thesis - Mid-Year Poster Presentation, Carnegie Mellon University
December 10, 2001
Parallel Theorem Proving for Linear Logic
ConCert Project Meeting, Carnegie Mellon University
October 31, 2001
An Application for a Certified Grid Computing Framework
Senior Research Thesis - Mid-Semester Presentation, Carnegie Mellon University
June 19, 2001
Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
PTP 2001: Workshop on Proof Transformations, Proof Presentations, and Complexity of Proofs