L. Bachmair and H. Ganzinger, Resolution theorem proving, Handbook of Automated Reasoning, vol.I, pp.19-99, 2001.

C. Ballarin, Locales: A module system for mathematical theories, J. Autom. Reasoning, vol.52, issue.2, pp.123-153, 2014.
DOI : 10.1007/s10817-013-9284-7
URL : http://www4.in.tum.de/~ballarin/publications/jar2013.pdf

R. J. Bayardo and R. Schrag, Using CSP look-back techniques to solve exceptionally hard SAT instances, LNCS, vol.96, pp.46-60, 1996.
DOI : 10.1007/3-540-61551-2_65
URL : http://www.bayardo.org/ps/cp96.pdf

H. Becker, J. C. Blanchette, M. Fleury, A. H. From, A. B. Jensen et al., IsaFoL: Isabelle Formalization of Logic

A. Biere and A. Fröhlich, Evaluating CDCL variable scoring schemes, SAT 2015, vol.5584, pp.237-243, 2015.
DOI : 10.1007/978-3-319-24318-4_29

A. Biere, M. Heule, and H. Van-maaren, Handbook of Satisfiability, vol.185, 2009.

J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reasoning, vol.56, issue.2, pp.155-200, 2016.
DOI : 10.1007/s10817-015-9335-3
URL : https://hal.archives-ouvertes.fr/hal-01211748

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT solvers, J. Autom. Reasoning, vol.51, issue.1, pp.109-128, 2013.
DOI : 10.1007/978-3-642-22438-6_11
URL : http://www.cl.cam.ac.uk/users/lcp/papers/Automation/cade2011-sledge-smt.pdf

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic proof and disproof in Isabelle/HOL, FroCoS 2011, vol.6989, pp.12-27, 2011.
DOI : 10.1007/978-3-642-24364-6_2
URL : http://www4.in.tum.de/%7Eblanchet/frocos2011-dis-proof.pdf

J. C. Blanchette, M. Fleury, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, IJCAR 2016, vol.9706, pp.25-44, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01592164

J. C. Blanchette and A. Popescu, Mechanizing the metatheory of Sledgehammer, FroCoS 2013, vol.8152, pp.245-260, 2013.

J. C. Blanchette, A. Popescu, and D. Traytel, Soundness and completeness proofs by coinductive methods, J. Autom. Reasoning, vol.58, issue.1, pp.149-179, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01643157

S. Böhme and T. Weber, Fast LCF-style proof reconstruction for Z3, ITP 2010, vol.6172, pp.179-194, 2010.

L. Bulwahn, A. Krauss, F. Haftmann, L. Erkök, and J. Matthews, Imperative functional programming with Isabelle/HOL, TPHOLs 2008, vol.5170, pp.134-149, 2008.

A. Church, A formulation of the simple theory of types, J. Symb. Log, vol.5, issue.2, pp.56-68, 1940.

L. Cruz-filipe, M. J. Heule, W. A. Jr, M. Kaufmann, and P. Schneider-kamp, Efficient certified RAT verification, CADE-26, vol.10395, pp.220-236, 2017.

M. Davis, G. Logemann, and D. W. Loveland, A machine program for theorem-proving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

N. Eén and N. Sörensson, An extensible SAT-solver, SAT 2003, vol.2919, pp.502-518, 2003.

M. Fleury, Formalisation of ground inference systems in a proof assistant, 2015.

M. Fleury and J. C. Blanchette, Formalization of Weidenbach's Automated Reasoning-The Art of Generic Problem Solving, 2018.

A. Goel and J. Grundy, Decision Procedure Toolkit

M. J. Gordon, R. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, vol.78, 1979.

F. Haftmann and T. Nipkow, Code generation via higher-order rewrite systems, FLOPS 2010, vol.6009, pp.103-117, 2010.

J. Harrison, Formalizing basic first order model theory, TPHOLs '98, vol.1479, pp.153-170, 1998.

F. Kammüller, M. Wenzel, and L. C. Paulson, Locales-A sectioning concept for Isabelle, TPHOLs '99, vol.1690, pp.149-166

. Springer, , 1999.

D. E. Knuth, Fascicle 6: Satisfiability, The Art of Computer Programming, vol.4, 2015.

A. Krauss, Partial recursive functions in higher-order logic, IJCAR 2006, vol.4130, pp.589-603, 2006.

S. Krsti´ckrsti´c and A. Goel, Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL, FroCoS 2007, vol.4720, pp.1-27, 2007.

P. Lammich, The Imperative Refinement Framework. Archive of Formal Proofs, 2016.

P. Lammich, Automatic data refinement, ITP 2013, vol.7998, pp.84-99, 2013.

P. Lammich, Refinement to Imperative/HOL, ITP 2015, vol.9236, pp.253-269, 2015.

P. Lammich, Refinement based verification of imperative data structures, CPP 2016, pp.27-36, 2016.

P. Lammich, Efficient verified (UN)SAT certificate checking, CADE-26, vol.10395, pp.237-254, 2017.

S. Lescuyer, Formalizing and implementing a reflexive tactic for automated deduction in Coq, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

M. Luby, A. Sinclair, and D. Zuckerman, Optimal speedup of Las Vegas algorithms, Inf. Process. Lett, vol.47, issue.4, pp.173-180, 1993.

J. Margetson and T. Ridge, Completeness theorem. Archive of Formal Proofs, 2004.

F. Mari´cmari´c, Formal verification of modern SAT solvers. Archive of Formal Proofs, 2008.

F. Mari´cmari´c, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theor. Comput. Sci, vol.411, issue.50, pp.4333-4356, 2010.

F. Mari´cmari´c and P. Jani?i´jani?i´c, Formalization of abstract state transition systems for SAT, Logical Methods in Computer Science, vol.7, issue.3, p.19, 2011.

J. P. Marques-silva and K. A. Sakallah, GRASP-A new search algorithm for satisfiability, ICCAD '96, pp.220-227, 1996.

R. Matuszewski and P. Rudnicki, Mizar: The first 30 years, Mechanized Mathematics and Its Applications, vol.4, issue.1, pp.3-24, 2005.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an efficient SAT solver, pp.530-535, 2001.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, vol.53, issue.6, pp.937-977, 2006.

T. Nipkow, Teaching semantics with a proof assistant: No more LSD trip proofs, VMCAI 2012, vol.7148, pp.24-38, 2012.

T. Nipkow and G. Klein, Concrete Semantics: With Isabelle/HOL, 2014.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.

D. Oe, A. Stump, C. Oliver, and K. Clancy, versat: A verified modern SAT solver, VMCAI 2012, vol.7148, pp.363-378, 2012.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, IWIL-2010, vol.2, pp.1-11, 2012.

B. C. Pierce, Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations, pp.121-122, 2009.

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, pp.195-202, 2014.

A. Schlichtkrull, Formalization of the resolution calculus for first-order logic, ITP 2016, vol.9807, pp.341-357, 2016.

N. Shankar, Metamathematics, Machines, and Gödel's Proof, vol.38, 1994.

N. Shankar and M. Vaucher, The mechanical verification of a DPLL-based satisfiability solver, Electr. Notes Theor. Comput. Sci, vol.269, pp.3-17, 2011.

N. Sörensson and A. Biere, Minimizing learned clauses, SAT 2009, vol.9340, pp.237-243, 2009.

C. Sternagel and R. Thiemann, An Isabelle/HOL formalization of rewriting for certified termination analysis

A. Voronkov, AVATAR: The architecture for first-order theorem provers, CAV 2014, vol.8559, pp.696-710, 2014.

C. Weidenbach, Automated reasoning building blocks, Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, vol.9360, pp.172-188, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239428

M. Wenzel, Isabelle/Isar-A generic framework for human-readable proof documents, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, vol.10, 2007.

N. Wirth, Program development by stepwise refinement, Commun. ACM, vol.14, issue.4, 1971.

J. Woodcock and R. Banach, The verification grand challenge, J. Univers. Comput. Sci, vol.13, issue.5, pp.661-668, 2007.