Computer Science and Engineering
University of California, San Diego
- Fall 2012
I joined the Programming Systems group, and am advised by Sorin Lerner and Ranjit Jhala.
- Summer 2011 - Summer 2012
I worked at Inria Paris-Rocquencourt in the Gallium team, under the supervision
of Xavier Leroy, on the CompCert C compiler project. More
tool for unformally validating the assembling and linking
process of CompCert-produced assembly files, according to the
PowerPC ABI. It proceeds by disassembling the produced ELF file and
matching it against the abstract assembly produced by the PowerPC
backend of CompCert.
A verified alias
analysis for the RTL intermediate language of CompCert.
This intra-procedural, flow-sensitive alias analysis proceeds according
to the famous Kildall data flow algorithm. The main challenge was to
come up with a proper representation for the data flow facts and the
invariants we maintain throughout the computation. Now that it is done,
the challenges remain to make it perform better (potentially by
reducing the unhelpful accuracy), and to leverage the results within
optimization passes (I did part of that on the common subexpression
elimination pass, but the proof is not complete).
Apprendre Haskell vous fera le plus grand bien, my French translation of
Learn You a Haskell for Great Good, by Miran Lipovaca.