A. Biere, PicoSAT essentials, Journal on Satisfiability Boolean Modeling and Computation (JSAT), vol.4, issue.2-4, pp.75-97, 2008.

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, Proc. of ITP 2010, pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: an open, trustable and efficient SMTsolver, Proc. of CADE 2009, 2009.
DOI : 10.1007/978-3-642-02959-2_12
URL : https://hal.archives-ouvertes.fr/inria-00430634

L. M. De-moura and N. Bjørner, Proofs and Refutations, and Z3, Proc. of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, 2008.

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Proc. of TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

L. M. De-moura, H. Rueß, and N. Shankar, Justifying Equality, Electronic Notes in Theoretical Computer Science, vol.125, issue.3, pp.69-85, 2005.
DOI : 10.1016/j.entcs.2004.06.068

L. M. De-moura, H. Rueß, and M. Sorea, Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proc. of CADE'02, pp.438-455, 2002.
DOI : 10.1007/3-540-45620-1_35

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

B. Dutertre and L. De-moura, The Yices SMT solver, 2006.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. F. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, Proc. of TACAS, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088

S. Mclaughlin, C. Barrett, and Y. 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.
DOI : 10.1016/j.entcs.2005.12.005

G. C. Necula, Compiling with Proofs, 1998.

G. C. Necula and P. Lee, Proof Generation in the Touchstone Theorem Prover, Proc. of CADE, pp.25-44, 2000.
DOI : 10.1007/10721959_3

R. Nieuwenhuis and A. Oliveras, Proof-Producing Congruence Closure, Proc. of RTA 2005, pp.453-468, 2005.
DOI : 10.1007/978-3-540-32033-3_33

A. Schrijver, Theory of Linear and Integer Programming, 1998.

A. Van-gelder, Verifying RUP proofs of propositional unsatisfiability, Elec. Proc. of ISAIM, 2008.

A. Van-gelder, Verifying Propositional Unsatisfiability: Pitfalls to Avoid, Proc of SAT'07, 2007.
DOI : 10.1007/978-3-540-72788-0_31

A. Van-gelder, Verifying RUP proofs of propositional unsatisfiability, Proc of ISAIM'08, 2008.

L. Zhang, Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications, Proc. of DATE 2003, pp.10880-10885, 2003.