S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken, The semantics of reflected proof, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.95-105, 1990.
DOI : 10.1109/LICS.1990.113737

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, pp.83-98
DOI : 10.1007/978-3-642-14052-5_8

URL : https://hal.archives-ouvertes.fr/inria-00502496

N. Ayache and J. C. Filliâtre, Combining the Coq proof assistant with first-order decision procedures, 2006.

T. Ball, E. Bounimova, V. Levin, R. Kumar, and J. Lichtenberg, The Static Driver Verifier Research Platform, CAV. LNCS, pp.119-122, 2010.
DOI : 10.1007/978-3-642-14295-6_11

M. Barnett, B. Y. Chang, R. Deline, B. J. Leino, and K. R. , Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO. LNCS, pp.364-387, 2005.
DOI : 10.1007/11804192_17

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, TYPES. LNCS, pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4

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

T. Bouton, D. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, CADE. LNCS, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38

URL : https://hal.archives-ouvertes.fr/inria-00430634

S. Conchon, E. Contejean, and J. Kanig, Ergo : a theorem prover for polymorphic first-order logic modulo theories, 2006.

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

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. D. Moura, The Yices SMT Solver, Tech. rep., SRI, 2006.

N. Eén and N. Sörensson, An Extensible SAT-solver, SAT. LNCS, pp.502-518, 2003.

J. C. Filliâtre and S. Conchon, Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML , ML '06, pp.12-19, 2006.
DOI : 10.1145/1159876.1159880

J. C. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, CAV. LNCS, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

P. Fontaine, J. Y. Marion, S. Merz, L. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS. LNCS, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26

URL : https://hal.archives-ouvertes.fr/inria-00001088

J. Franco and J. Martin, A History of Satisfiability, Handbook of Satisfiability, pp.3-74, 2009.

G. Gonthier, A computer-checked proof of the four colour theorem, Tech. rep., Microsoft Research Cambridge, 2005.

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, pp.235-246, 2002.

B. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, FLOPS. LNCS, pp.97-113, 2006.
DOI : 10.1007/11737414_8

J. Harrison, Formal Proof ? Theory and Practice, Notices of the American Mathematical Society, vol.55, 2008.

C. Kaliszyk and F. Wiedijk, Certified Computer Algebra on Top of an Interactive Theorem Prover, Calculemus/MKM, pp.94-105, 2007.
DOI : 10.1007/978-3-540-73086-6_8

M. Kaufmann and L. C. Paulson, Interactive Theorem Proving, Proceedings, Lecture Notes in Computer Science, vol.6172, 2010.
DOI : 10.1007/978-3-642-14052-5

M. Kawaguchi, P. M. Rondon, and R. Jhala, Dsolve: Safety Verification via Liquid Types, CAV. LNCS, pp.123-126, 2010.
DOI : 10.1007/978-3-642-14295-6_12

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814

URL : https://hal.archives-ouvertes.fr/inria-00415861

S. Lescuyer and S. Conchon, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, FroCos. LNCS, pp.287-303, 2009.
DOI : 10.1016/j.jal.2007.07.003

J. Marques-silva, Practical applications of Boolean Satisfiability, 2008 9th International Workshop on Discrete Event Systems, 2008.
DOI : 10.1109/WODES.2008.4605925

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

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

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

N. Tillmann and J. De-halleux, Pex???White Box Test Generation for .NET, TAP. LNCS, pp.134-153, 2008.
DOI : 10.1007/978-3-540-79124-9_10

T. Weber, SAT-based Finite Model Generation for Higher-Order Logic, 2008.