office ECOT 621
mail 430 UCB, Boulder, CO 80309-0430 USA
phone +1 303 492 8894
fax +1 303 492 2844
zoom 303 492 8894

Postdoc Position. There is a postdoctoral research associate position open with the opportunity to work with me and others in the CUPLV group.

Ph.D. Positions. I am always looking for enthusiastic students interested in working with me on research projects in programming languages and software systems. If you are interested in finding out more, please contact me.

For recent news about the Programming Languages group at the University of Colorado Boulder, take a look at our most recent recruiting talk.

I am an assistant professor in the Department of Computer Science and the Programming Languages and Verification Group at the University of Colorado Boulder.

I work primarily in the areas of programming languages and program analysis. My research interests center on tools and techniques for building, understanding, and ensuring reliable computational systems. Currently, my focus is on using novel ways of interacting with the programmer to design more precise and practical program analyses. The Xisa project is an instance of this approach that infers precise properties of complex data structure manipulations. The novelty of Xisa is that it extracts both the necessary invariants and reasoning rules from executable assertions (analogous to data structure validation code often written for testing). This approach allows the developer to focus the analysis to the properties of interest and without using a separate formalism for testing and static analysis.

I completed my Ph.D. in 2008 with George Necula in the EECS department at the University of California, Berkeley. I also spent the fall of 2008 as a post-doc with Jeff Foster in the PLUM group at the University of Maryland, College Park before joining the University of Colorado Boulder in January 2009.

Even earlier, I spent my undergraduate days at Carnegie Mellon University completing a senior thesis with Frank Pfenning and Bob Harper.

Students

Modular verification of almost-everywhere invariants: method reflection, Objective-C

Abstract domain combinators for dynamic languages: reflective metaprogramming frameworks, JavaScript. Co-advised with Sriram Sankaranarayanan.

Precise refutation analysis: may-witnesses, false alarm triage, Android, Java.

Yi-Fan Tsai

Incremental verification-validation: data structure invariants, incrementalization, C.

Teaching

Compiler Construction
CSCI 4555/5525, ECEN 4553/5523
Program Analysis: Theory and Practice
CSCI 7135
Principles of Programming Languages
CSCI 3155
Readings in Programming Languages
Spring 2012: Analysis of Dynamic Languages
CSCI 7900
Program Analysis Practicum
CSCI 7135
Fundamentals of Programming Languages
CSCI 5535

Selected Projects

DroidelA Framework Model for Static Analysis of Android Applications

A community-driven modeling of the Android framework for static analysis of Android applications. Droidel seeks to be a general purpose model for static analysis based on minimal explication of dynamism in the Android framework code.

References: SOAP 2015
QUIC GraphsRelational Invariant Generation for Containers

An abstract domain constructor for inferring invariants about sets and set properties of containers.

References: ECOOP 2013
ThresherPrecise Refutations for Heap Reachability

A static analysis tool for Java programs that specializes in checking heap reachability properties and provides automated alarm triage assistance.

References: PLDI 2013
Fissile Type AnalysisModular Checking of Almost-Everywhere Invariants

A static analysis tool for C and Objective-C that verifies invariants that hold almost everywhere, including the safety of reflective method calls.

References: POPL 2014
XisaExtensible Inductive Shape Analysis

Efficient algorithms and automatic tools for reasoning about heap-manipulating programs, such as those that use recursive data structures like pointer-based lists and trees.

Recent Papers

2015
Droidel: A General Approach to Android Framework Modeling
SOAP 2015: ACM SIGPLAN Workshop on State of the Art in Program Analysis
2015
Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages
ESOP 2015: European Symposium on Programming
2014
Construction of Abstract Domains for Heterogeneous Properties (Position Paper)
ISOLA 2014: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
2014
Automatic Analysis of Open Objects in Dynamic Language Programs
SAS 2014: International Static Analysis Symposium
2014
An Abstract Domain Combinator for Separately Conjoining Memory Abstractions
SAS 2014: International Static Analysis Symposium
[more]

Recent Talks

May 18, 2015
Type-Intertwined Heap Analysis
Aarhus University. Aarhus, Denmark.
February 25, 2015
Fixr: Mining and Understanding Bug Fixes for App-Framework Protocol Defects
DARPA MUSE Site Visit. University of Colorado Boulder. Boulder, Colorado, USA.
October 15, 2014
Fixr: Mining and Understanding Bug Fixes for App-Framework Protocol Defects
DARPA MUSE Kickoff. Annapolis, Maryland, USA
September 22, 2014
Cooperative Program Analysis
Colorado State University. Fort Collins, Colorado, USA.
August 6, 2014
Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants
Japan Advanced Institute of Science and Technology. Nomi, Japan.
[more]

Professional Activities

POPL 2016
Program Committee Member
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
VSTTE 2015
Program Committee Member
IFIP Working Conference on Verified Software: Theories, Tools, and Experiments
PLDI 2015
External Review Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
POPL 2015
External Review Committee Member
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
POPL 2014
Co-Treasurer
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
TAPAS 2013
Program Committee Chair
International Workshop on Tools for Automatic Program Analysis
POPL 2013
Treasurer
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
TAPAS 2012
Program Committee Member
International Workshop on Tools for Automatic Program Analysis
PLDI 2012
External Review Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
POPL 2012
Treasurer and External Review Committee Member
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
VMCAI 2012
Program Committee Member
International Conference on Verification, Model Checking, and Abstract Interpretation
NSAD 2011
Program Committee Member
International Workshop on Numerical and Symbolic Abstract Domains
LCPC 2011
Program Committee Member
International Workshop on Languages and Compilers for Parallel Computing
PASTE 2011
Program Committee Member
ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering
POPL 2011
Treasurer
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
POPL 2010
Co-Treasurer
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
FRACTAL F2009
Organizer
Front Range Architecture Compilers Tools and Languages Workshop
PLDI 2009
External Review Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
AIOOL 2005
Program Committee Member
International Workshop on Abstract Interpretation of Object-Oriented Languages