What's new

July 2017
A new draft is available. The title is Bounded Expectations: Resource Analysis for Probabilistic Programs and this is joint work with Chan Ngo and Quentin Carbonneaux.
June 2017
I will join the ICALP 2018 program committee.
June 2017
I am looking forward to co-chair the 19th Workshop on Logic and Computational Complexity (LCC’18) with Erich Graedel. Details will follow.
June 2017
I am excited that our paper Arrays and References in Resource Aware ML (with Ben Lichtman) will be presented at FSCD'17.
May 2017
I am honored to be an invited speaker at the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '17). I hope to see you on July 22-23 at Heidelberg.
April 2017
I'm excited that our paper Automated Resource Analysis with Coq Proof Objects has been accepted to the 29th International Conference on Computer-Aided Verification (CAV'17). Thanks to my co-authors Quentin Carbonneaux, Tom Reps, and Zhong Shao.
April 2017
I'm looking forward to teach 15-411/611 Compiler Design in Fall.
February 2017
Our paper Verifying and Synthesizing Constant-Resource Implementations with Types (with Van Chan Ngo, Mario Dehesa-Azuara, and Matt Fredrikson) has been conditionally accepted to the 2017 IEEE Symposium on Security & Privacy (Oakland).
December 2016
Great news: Our paper ML for ML: Learning Cost Semantics by Experiment (with Ankush Das) has been accepted to TACAS 2017.
December 2016
I'm looking forward to be a member of the FOPARA-DICE 2017 and ESOP 2018 program committees. Please submit your latest and greatest work.
December 2016
I'm excited to co-teach 15-312 Principles of Programming Languages with Bob Harper next semester.
October 2016
We just finished two new manuscripts. The titles are ML for ML: Learning Cost Semantics by Experiment (with Ankush Das) and Arrays and References in Resource Aware ML (with Ben Lichtman). Comments are very welcome.
October 2016
I'm very excited that I'm the co-author of two POPL'17 papers. The first one, titled Relational Cost Analysis, a result of an collaboration with Ezgi Cicek, Gilles Barthe, Marco Gaboardi, and Deepak Garg. (A draft will be available online shortly.) The second one is Towards Automatic Resource Bound Analysis for OCaml, which is co-authored by Ankush Das and Shu-Chun Weng. I am looking forward to seeing you all in Paris.
July 2016
Try out the new version 1.30 of RAML. It can now derive lower bounds and verify that a program uses a constant amount of resources.
July 2016
I'm very excited about our work on Quantifying and Preventing Side Channels with Substructural Type Systems. This is joint work with Chan, Matt, and Mario (now at Jane Street).
July 2016
Check out Ankush's work on Learning Cost Semantics for Modeling Running Time of OCaml Programs, which he presented at LOLA 2016.

What was new

June 2016
I'm deligted to server on the programm committee of Formal Structures for Computation and Deduction (FSCD'17) next year. Please consider submitting.
April 2016
Together with Marco Gaboardi, I am co-chairing LOLA 2016, a satellite workshop of LICS 2016 in New York City. Please submit exciting talk proposals.
April 2016
We (with Marco Gaboardi, Reinhard Wilhelm, and Florian Zuleger) have been selected to organize a Dagstuhl Seminar on Resource-Bound Analysis. The seminar will be amazing and will be held from July 16 to July 21, 2017.
April 2016
I'm looking forward to teach course 15-411/15-611 (Compiler Design) in Fall 2016.
March 2016
I will be a member of the PLDI'17 Program Committee. Please submit your most amazing papers. (Thanks to PC Chair Martin Vechev for inviting me.)
February 2016
I am thrilled to receive a Google Research Award.
December 2015
I am looking forward to speak about Automatic Resource-Bound Analysis at the 2016 Oregon Programming Languages Summer School.
December 2015
Together with Andrew Appel and others, I will give a tutorial on Foundational Verification of Real Systems in the Large at MFPS'16.
December 2015
I will teach 15-819 Advanced Topics in Programming Languages: Resource Analysis in Spring 2016.
November 2015
I am very excited about the new version of Resource Aware ML (RAML). It now analyzes (higher-order) OCaml code. For details check out the new RAML website.
September 2015
I will serve on the FoSSaCS'16 Program Committee and on the CAV'16 External Review Committee. Please consider submitting.
September 2015
I started as Tenure-Track Assistant Professor in Carnegie Mellon's Computer Science Department.
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.
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.