What's new

May 2018
I am co-organizing two events at FLOC 2018. LCC'18 will be on July 13, 2018 and features a memorial session for my friend and PhD advisor Martin Hofmann (1965-2018) in the afternoon. The Logic Mentoring Workshop will take place on July 8, 2018. We have an exciting group of panelists and speakers and I am sure that students will enjoy the workshop.
May 2018
Our paper (with Ankush Das and Frank Pfenning) Parallel Complexity Analysis with Temporal Session Types has been conditionally accepted to ICFP 2018.
April 2018
The second part of our (with Ankush and Frank) work on resource analysis for session types is online: Parallel Complexity Analysis with Temporal Session Types . I think it's a novel and beautiful approach to resource analysis. You should read it.
April 2018
I am excited that our paper Work Analysis with Resource-Aware Session Types (with Ankush Das and Frank Pfenning) will appear at LICS 2018.
February 2018
I'm looking forward to serving on the POPL 2019 program committee. Thanks, PC chair Stephanie Weirich.
February 2018
I am very happy that two papers on probabilistic programming have been conditionally accepted to PLDI 2018. The first one is PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs with Di Wang and Tom Reps. The second one is Bounded Expectations: Resource Analysis for Probabilistic Programs with Chan Ngo and Quentin Carbonneaux. Congratulations to the lead authors Di and Chan.
February 2018
A new working paper is available: A Denotational Semantics for Nondeterminism in Probabilistic Programs. This is a collaboration with Di Wang and Tom Reps.
December 2017
I'm very excited to give an invited talk at DICE 2018. The topic will likely be automatic resource analysis for probabilistic programs. I hope to see you at DICE soon.
December 2017
I joined the PLDI 2018 Student Research Competition PC.
November 2017
Check out our latest work titled PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs. This is joint work with Di Wang and Tom Reps, and my first collaboration with my new student Di.
November 2017
A new version of our paper Bounded Expectations: Resource Analysis for Probabilistic Programs is available (joint work with Chan and Quentin). It now contains an impressive experimental evaluation.
October 2017
A new paper by Ankush Das, Frank Pfenning, and me about Work Analysis with Resource-Aware Session Types is online.
October 2017
I'm looking forward to teaching 15-312 Foundations of Programming Languages in Spring 2018. (Many thanks to Bob Harper for the opportunity.)
September 2017
I am very excited that I will advice Di Wang during his PhD studies at Carnegie Mellon. Welcome Di!
September 2017
Quentin Carbonneaux (PhD) graduated this summer. Quentin wrote a fantastic PhD thesis titled Modular and Certified Resource-Bound Analyses. Some of the results have been published at PLDI and CAV but there's a lot more material in the thesis that would be well-suited for a conference publication. Congratulations Quentin! (Quentin took a position at Google.)
September 2017
Ben Lichtman (BS) graduated this summer with a very strong senior thesis is titled Resource Aware Program Synthesis and a publication at FSCD. Congrats Ben! (Ben took a position at Microsoft.)

What was 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 Foundations 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.
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.