F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3 : Shepherd Your Herd of Provers, International Workshop on Intermediate Verification Languages (Boogie), 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-Calculus Modulo as a Universal Proof Language, Proof Exchange for Theorem Proving (PxTP), 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, LPAR ? Springer LNCS/LNAI 4790, 2007.
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920

G. Burel, Experimenting with Deduction Modulo, CADE ? Springer LNCS/LNAI 6803, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

G. Burel, A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo, Proof Exchange for Theorem Proving (PxTP) ? EasyChair EPiC 14, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LPAR ? Springer LNCS/ARCoSS 8312, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, ABZ ? Springer LNCS 7316, 2012.
DOI : 10.1007/978-3-642-30885-7_17