Interest scope and activities
I am interested in research about formal methods, formal proof, decision procedures and proof assitants.
- My thesis "Applying result certification to automatize interactive proofs" is about the validation of proofs generated by an external solver using its own decision procedure, in order to build a proof in another, more reliable system such as proof assistants. More specificaly, I worked on applying this verification techniques to link SMT Solvers such as VeriT in the proof assistant Coq.
- I was part of the ANR Decert project, which intent was to design an architecture for cooperating decision procedure.