What's new

July 2015
I'm very excited about a project with Shu-Chun Weng in which we develop an automatic resource bound analysis for OCaml. A manuscript of a recent conference submission can be found here. More info will follow soon.
July 2015
Our article Type-Based Amortized Resource Analysis with Integers and Arrays has been accepted for publication at the Journal of Functional Programming. This is the journal version of a joint conference article with Zhong that appeared at FLOPS 2014.
July 2015
I'm looking for a post-doc to work with me on a project related to resource bound analysis and security at Carnegie Mellon University. Please get in touch if you are interested in the position.
June 2015
I will start as Tenure-Track Assistant Professor at Carnegie Mellon's Computer Science Department in fall 2015. Many thanks to everyone who supported me during the job search.
May 2015
We created a video abstract for our upcoming PLDI 2015 paper Compositional Certified Resource Bounds. I hope to see you at my talk on Wed, June 17.
February 2015
Our article Compositional Certified Resource Bounds will appear at PLDI 2015. I hope to see you in June at the talk in Portland. This is joint work with Quentin and Zhong. More infos and an online demo are available on the project website.

What was new

December 2014
I'm on the academic job market this year. Please contact me for my application package.
December 2014
Fantastic news! Our paper Automatic Cost Analysis for Parallel Programs (joint work with Zhong Shao) has been accepted for publication at ESOP 2015. I hope to see you at the talk at ETAPS in London in April.
July 2014
Take a look at my latest research on Compositional Certified Resource Bounds. Finally, we have an automatic amortized analysis that works well for system code written in C. This is joint work with Quentin and Zhong. More infos and an online demo can be found on the project website.
February 2014
A new paper on automatic amortized analysis will appear at FLOPS 2014. The title is Type-Based Amortized Resource Analysis with Integers and Arrays and this is joint work with Zhong.
February 2014
Our paper End-to-End Verification of Stack-Space Bounds for C Programs has been selected for publication at PLDI 2014. This is joint work with Quentin, Tahina, and Zhong. Also check out the project web site.
November 2013
Quentin, Tahina, Zhong, and I have submitted a paper on a new framework for formally verifying stack bounds of compiled x86 assembly code at the C level. The title is End-to-End Verification of Stack-Space Bounds for C Programs.
September 2013
Gabriel Scherer and I got a paper accepted at LPAR'13. The title is Tracking Data-Flow with Open Closure Types.
August 2013
Take a look at our (with Zhong) new draft: Towards Amortized Resource Analysis for Imperative Programs.
July 2013
The NSF has awarded Zhong and me a research grant for the VeriQ project. In this project we investigate formal verification of resource-usage information and other quantities properties of software. The funding is for three years.
May 2013
Our paper Characterizing Progress Properties of Concurrent Objects via Contextual Refinements will appear in the proceedings of CONCUR 2013. This is joint work with Hongjin Liang, Xinyu Feng, and Zhong Shao.
May 2013
Amortized resource analysis also works for parallel evaluation! Check out my latest research on Automatic Cost Analysis for Parallel Programs (joint work with Zhong Shao).
February 2013
Our paper Quantitative Reasoning for Proving Lock-Freedom has been accepted for publication at LICS 2013. This is joint work with Michael Marmar and Zhong Shao.
August 2012
Our article Multivariate Amortized Resource Analysis (joint work with Klaus and Martin) has been accepted to TOPLAS. The final version of the artical is now available online.
February 2012
Our tool paper on Resource Aware ML has been accepted to CAV 2012 (joint work with Klaus and Martin). I hope to see you at our tool demo in Berkeley.
October 2011
I successfully defended my doctoral thesis on October 14, 2011. My dissertation with the title Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis is available online. It contains a thorough informal introduction to my research topic.