1. Combinatorial optimization, Operational research
• Graph theory, perfect graphs
• Algorithmic complexity
• Mathematical programming
• Approximation
2. Partial path covering
• Minimum partial multicut
• Minimum disjoint paths blocker
3. Graph-Coloring-based register allocation
• Coalescing
• Live-Range splitting
4. Formal verification
• Formal verification of operational research algorithms
• Development of specification helpful tools for combinatorial optimization research

My Ph. D. takes place in the CompCert project, whose supervisor is Xavier Leroy. This project aims at the Coq development of a formally verified optimizing static compiler for Clight, a large subset of C, to be used for critical embedded software. The current release for this compiler is available here. It produces code of good quality (a little bit slower than gcc's first level of optimization). Current work focus on compiler optimizations.