G. Burel, Experimenting with Deduction Modulo, Conference on Automated Deduction, pp.162-176, 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), pp.43-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

D. Déharbe, P. Fontaine, Y. Guyot, and L. Voisin, SMT Solvers for Rodin, ABZ [1], pp.194-207
DOI : 10.1007/978-3-642-30885-7_14

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps, International Workshop on the Implementation of Logics (IWIL), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00909688

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, Logic for Programming Artificial Intelligence and Reasoning (LPAR), pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, ESOP, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, ABZ [1], pp.238-251
DOI : 10.1007/978-3-642-30885-7_17

D. Mentré, C. Marché, J. Filliâtre, and M. Asuka, Discharging Proof Obligations from Atelier??B Using Multiple Automated Provers, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), pp.238-251, 2012.
DOI : 10.1007/978-3-642-30885-7_17