Situation

I defended my PhD in February 2012, and made a five months visit at CSAIL, in Adam Chlipala's group.

In September 2012, I started a post-doc in the Gallium team, at Inria Rocquencourt.

News

• Publication: "Fe-Si : Formal Verification of Hardware Synthesis" with Adam Chlipala, to be presented at CAV 2013 (find more here)
• Paper submitted. "Implementing hash-consed structures in Coq" (with Jacques-Henri Jourdan and David Monniaux, draft here)
• A talk at the Coq workshop 2012 .pdf

PhD

During my PhD, we released a reflexive tactic for deciding Kleene algebras; the current state of the corresponding library (ATBR) can be found here. We also implemented tools for rewriting modulo AC in Coq; the current state of the corresponding library can be found here.

Toward the end of my PhD, I implemented a Coq library for verifying hardware; the (outdated) state of the corresponding library can be found here.

Research

My current research interests involve the use of the Coq proof assistant to verify hardware components.

Tools

I am a happy user of the Coq proof assistant, and do most of my software developments in OCaml.