M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry-&-benjamin et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP 2011, vol.7086, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

H. Barbosa, J. C. Blanchette, and M. Fleury-&-pascal-fontaine, Scalable Fine-Grained Proofs for Formula Processing, Journal of Automated Reasoning, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01526841

H. Barbosa, J. C. Blanchette, M. Fleury, P. Fontaine, &. Hans-jörg et al., Better SMT proofs for easier reconstruction, 2019.

C. Barrett, P. Fontaine-&-cesare, and . Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.

C. Barrett, R. Sebastiani, S. Seshia-&-cesare, and . Tinelli, Satisfiability Modulo Theories, Handbook of Satisfiability, vol.26, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

, A Flexible Proof Format for SMT: A Proposal, pp.15-26, 2011.

C. Jasmin, S. Blanchette, M. Böhme, S. J. Fleury, A. Smolka et al., Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.56, issue.2, pp.155-200, 2016.

S. Böhme and &. Weber, Fast LCF-Style Proof Reconstruction for Z3, ITP 2010, vol.6172, pp.179-194, 2010.

T. Bouton, C. B. Diego, D. De-oliveira, and . Fontaine, veriT: An Open, Trustable and Efficient SMT-solver, CADE 2009, vol.5663, pp.151-156, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430634

S. Buchwald and D. Lohner-&-sebastian-ullrich, Verified construction of static single assignment form, CC, ACM, pp.67-76, 2016.

D. Déharbe, P. Fontaine, &. Bruno-woltzenlogel, and . Paleo, Quantifier Inference Rules for SMT Proofs, pp.33-39, 2011.

B. Ekici, G. Katz, C. Keller, A. Mebsout, and A. J. Reynolds-&-cesare-tinelli, Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), EPTCS, vol.210, pp.21-29, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01388984

S. Mclaughlin and C. Barrett-&-yeting-ge, Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.43-51, 2006.

, Z3: An Efficient SMT Solver, TACAS 2008, vol.4963, pp.337-340, 2008.

A. Schlichtkrull and J. C. Blanchette, Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Archive of Formal Proofs, Dmitriy Traytel & Uwe Waldmann, 2018.

A. Schlichtkrull and J. C. Blanchette, Formalizing Bachmair and Ganzinger's Ordered Resolution Prover, IJCAR, LNCS 10900, pp.89-107, 2018.

A. Schrijver, Theory of Linear and Integer Programming. Wiley -Interscience Series in Discrete Mathematics and Optimization, 1999.

A. Stump, D. Oe, and A. Reynolds, SMT Proof Checking Using a Logical Framework, Liana Hadarean & Cesare Tinelli, vol.42, issue.1, pp.91-118, 2013.

S. Ullrich and &. Lohner, Verified Construction of Static Single Assignment Form. Archive of Formal Proofs, 2016.