Quentin Carbonneaux

first name dot c9x @gmail.com

This is my old academic page hosted by Yale University. I now work as software engineer in Google Brain. I completed my PhD studies in August 2017 at Yale University where my advisor was Professor Zhong Shao.

If you are interested in the analysis of the resource usage of low-level programs (e.g., to verify embedded systems, or improve your developers' static analysis toolkit), you should take a look at my dissertation.

My interests range from low level system design and hacking to logic, proof assistants and algebra. I like to talk about bits and bytes in sound mathematical frameworks. I spend a good amount of free time writing compilers of any kind. My personal website contains lots of non-work-related goodies.

News

• As of September 2017, I am software engineer in Google Brain.

• As of May 2017, I am working on my Ph.D. dissertation to graduate in early August 2017.

• On November 4th 2015, for the Yale PL day, I presented some slides on Invariant Logics. These logics help proving that a program preserves an arbitrary invariant throughout its whole execution. You can checkout the accompanying (and suprisingly short) Coq development.

• In April 2015 I made some slides to help me make a smooth yet technical presentation of the resource bound problem for imperative languages.

• I am working on the implementation of a tool to derive worst-case resource bounds automatically on C code. The project has its own page with an online demo and Coq proofs of the system. In June 2015, we presented the current state of the project at PLDI, see below.

Publications

• I am excited that, with the help of Van Chan Ngo and Jan Hoffmann, we extended my previous work to be available for probabilistic programs. The bounds we derive are now on the expected resource consumption. We are glad that, again, our tool was validated by the conference's Artifact Evaluation Committee.

  V. C. Ngo, Q. Carbonneaux, J. Hoffmann. Bounded Expectations: Resource Analysis for Probabilistic Programs, in PLDI'18. (pdf)

• After the PLDI'15 work, I decided to break our system in little orthogonal pieces to understand what it was really made of. This analysis laid the foundations for a new tool: Pastis. Pastis can infer, but is not limited to, polynomial bounds. Thanks to the cleanup, it can also generate small and clean Coq certificates proving the validity of the bounds it found. This work was accepted into CAV'17 and Pastis was validated by the Artifact Evaluation Committee.

  Q. Carbonneaux, J. Hoffmann, T. Reps, Z. Shao. Automated Resource Analysis with Coq Proof Objects, in CAV'17. (pdf)

• I am really glad that my work on automating resource analysis for C programs has been accepted into PLDI'15. Our implementation has been validated by the Artifact Evaluation Committee of the conference!

  Q. Carbonneaux, J. Hoffmann, Z. Shao. Compositional Certified Resource Bounds, in PLDI'15. (pdf) (technical report) (video abstract)

• 

  If you are worried about the stack usage of your embedded system's firmware written in C, this work provides formal tools to bound the stack consumption of the compiled code by resoning on the source.

  Q. Carbonneaux, J. Hoffmann, T. Ramananandro, Z. Shao. End-to-end Verification of Stack-space Bounds for C Programs, in PLDI'14. (pdf) (technical report) (Coq development) (poster) (stack monitoring program for Linux)

  The poster was presented during the POPL'14 poster session.

• N. Lebert, F. Meunier, Q. Carbonneaux. Envy-free two-player m-cake and three-player two-cake divisions, in "Operations Research Letters", 2013. (on HAL)

• For my master's thesis, I developed a very efficient type checker for an extensible lambda calculus with dependent types: Dedukti. This type checker benefits from state of the art JIT compilers to normalize computationally intensive proofs. My thesis was supervised by Gilles Dowek, Olivier Hermant, and Mathieu Boespflug. Most of this work is based on Mathieu Boespflug's PhD thesis.

  Q. Carbonneaux. Compilation JIT des termes de preuve, 2012 (pdf in French) (slides in English)

• M. Boespflug, Q. Carbonneaux, O. Hermant. The λΠ-calculus Modulo as a Universal Proof Language, in PxTP'12 (Proof Exchange for Theorem Proving). (pdf) (slides)

• In 2011 I was intern in Pierre Weis's research group at INRIA Rocquencourt. Together with Pierre Weis and François Clément we developed a user friendly and type safe DSL to express parallel computations in OCaml. The implementation called Sklml can be downloaded and tried with recent (≥ 3.12) OCaml versions.

Teaching at Yale & Service

• October 2015 - I was member of the Artifact Evaluation Committee for POPL 2016.

• Fall 2016 - Teaching Fellow for CS 422: Design and Implementation of Operating Systems.
  Professor: Zhong Shao.

• Spring 2015 - Teaching Fellow for CS 421: Compilers and Interpreters.
  Professor: Zhong Shao.

• Fall 2014 - Teaching Fellow for CS 454: Software Verification and Analysis.
  Professor: Ruzica Piskac.

• Spring 2014 - Teaching Fellow for CS 421: Compilers and Interpreters.
  Professor: Zhong Shao.

• Fall 2013 - Teaching Fellow for CS 323: Introduction to Systems Programming and Computer Organization.
  Professor: Stanley Eisenstat.