With Anne Pacalet.
A pre-condition algorithm on C with correctness proof in Coq. For the Frama-C project.