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

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 insight into the Programming Languages and Verification group, take a look at a recent recruiting talk.

I am an Associate Professor in the Department of Computer Science and the Department of Electrical, Computer, and Energy Engineering (by courtesy) at the University of Colorado Boulder. I co-direct the Programming Languages and Verification Group (CUPLV). I am also a Scholar with Amazon.

My research focuses on making software better and programmers more productive by investigating the fundamental principles and techniques needed to algorithmically assist the software developer throughout the software engineering process. Our advances seek to help users better specify what they care about, interact with automated reasoning engines, triage the alarms from tools, and leverage source code repositories to improve their software. This work is often driven the needs of today's real-world applications to ultimately inform tomorrow's designs.

I completed my Ph.D. with George Necula at the University of California, Berkeley and spent a semester as a postdoctoral researcher with Jeffrey S. Foster in the PLUM group at the University of Maryland, College Park before joining the University of Colorado Boulder.

Current PhD Students

Termination, complexity, and cost analysis: denial-of-service, algorithmic security vulnerabilities, Java. Co-advised with Pavol Černý.

Specification and verification of event-driven systems: lifestate specifications, specification mining, callbacks, Android.

Graduated PhD Students

Precise refutation analysis: heap reachability, may-witnesses, false alarm triage, memory leaks, Android, Java.

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.

Incremental and demand driven abstract interpretation; goal-directed abstract interpretation for dynamic languages.

Past Research Scientists

Edmund S.L. Lam

Mining and understanding bug fixes for app-framework protocol defects: property-based testing of interactive apps, big data pipelines.

Past Post-Doctoral Fellows

Mining and understanding bug fixes for app-framework protocol defects: event-based object protocol verification.

Graduated MS Students

Yi-Fan Tsai

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

Teaching

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

Selected Projects

Fixr
Mining and Understanding Bug Fixes for App-Framework Protocol Defects

Developing program analysis, probabilistic inference, program synthesis, social data mining, and big-data engineering tools to cooperative repair Android framework protocol misuses.

Droidel
A 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 Graphs
Relational Invariant Generation for Containers

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

References: ECOOP 2013
Thresher
Precise 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 Analysis
Modular 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
Xisa
Extensible 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.

Demanded Abstract Interpretation
Expressive and Interactive Static Analysis

A framework for incremental and demand-driven compositional abstract interpretation in arbitrary abstract domains and without loss of precision.

References: PLDI 2021

Recent Papers

2023
Historia: Refuting Callback Reachability with Message-History Logics
OOPSLA 2023: ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
2022
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
Ðorđe Žikelić, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi
PLDI 2022: ACM SIGPLAN Conference on Programming Language Design and Implementation
2021
Selectively-Amortized Resource Bounding
SAS 2021: International Static Analysis Symposium
2021
Demanded Abstract Interpretation
PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
2020
Shape Analysis
Foundations and Trends in Programming Languages (FnTPL) Found. Trends Program. Lang.
[more]

Recent Talks

February 1, 2016
Fixr: Mining and Understanding Bug Fixes for App-Framework Protocol Defects
DARPA MUSE Demonstration Workshop. Arlington, Virginia, USA.
October 3, 2015
Goal-Directed Program Analysis with Jumping
Max Planck Institute for Software Systems. Kaiserslautern, Germany.
October 1, 2015
Goal-Directed Program Analysis with Jumping
École Normale Supérieure. Paris, France.
July 24, 2015
Goal-Directed Program Analysis with Jumping
Google. Mountain View, California, USA.
July 22, 2015
Fixr: Mining and Understanding Bug Fixes for App-Framework Protocol Defects
DARPA MUSE PI Meeting. SRI International. Menlo Park, California, USA.
[more]

Professional Activities

SPLASH 2022
Sponsorship Co-Chair
ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity
CAV 2022
Program Committee Member
International Conference on Computer Aided Verification
PLDI 2022
Program Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
CAV 2021
Program Committee Member
International Conference on Computer Aided Verification
CAV 2021
Sponsorship Chair
International Conference on Computer Aided Verification
PLDI 2021
Program Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
SAS 2020
Program Committee Member
International Static Analysis Symposium
PLDI 2020
External Review Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
POPL 2020
Program Committee Member
ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
OOPSLA 2019
Review Committee Member
ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications
SAS 2019
Program Committee Chair
International Static Analysis Symposium
ISSTA 2019
Program Committee Member
International Symposium on Software Testing and Analysis
SAS 2018
Program Committee Member
International Static Analysis Symposium
ASPLOS 2018
External Review Committee Member
ACM International Conference on Architectural Support for Programming Languages and Operating Systems
APLAS 2017
Program Committee Chair
Asian Symposium on Programming Languages and Systems
ECOOP 2017
Program Committee Member
European Conference on Object-Oriented Programming
PLDI 2017
Program Committee Member
ACM SIGPLAN Conference on Programming Language Design and Implementation
APLAS 2016
Program Committee Member
Asian Symposium on Programming Languages and Systems
SAS 2016
Program Committee Member
International Static Analysis Symposium
VMCAI 2016
Program Committee Member
International Conference on Verification, Model Checking, and Abstract Interpretation
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