Modular SMT Proofs for Fast Reflexive Checking Inside Coq. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (CPP, 2011)

A Nelson-Oppen based Proof System using Theory Specific Proof Systems. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (PxTP, 2011)

Walking through the Forest: Fast EUF Proof-Checking Algorithms. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Ronan Saillard (PxTP, 2012)

Result Certification of Static Program Analysers with Automated Theorem Provers. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Thomas P. Jensen (VSTTE, 2013)

Certification of static analysis in many-sorted first-order logic. (Analyse statique certifiée en logique du premier ordre multi-sortée). - Pierre-Emmanuel Cornilleau (2013)