Valentin Robert
vrobert@cs.ucsd.edu
PhD Student
Computer Science and Engineering
University of California, San Diego
Curriculum Vitae
Research
- Summer 2013
I interned at Microsoft Research Cambridge, Programming Principles and Tools group under the supervision of Andrew Kennedy working on issues with modular verification of low-level assembly code.
- Fall 2012
I joined the Programming Systems group, and am advised by Sorin Lerner.
- 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
specifically:
-
Checklink, a
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).
Publications
Blog posts
Miscellaneous
Apprendre Haskell vous fera le plus grand bien, my French translation of
Learn You a Haskell for Great Good, by Miran Lipovaca.
I once attempted to explain coinduction to my coworkers.
I gave my research examination on the subject of proof-assistant-based verification of programs.
