G. Audemard and L. Simon, Predicting learnt clauses quality in modern SAT solvers, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp.399-404, 2009.

L. Bachmair, H. Ganzinger, D. Mcallester, and C. Lynch, 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, 2013.

T. Balyo and M. J. Heule, SAT Competition 2018: Solver and Benchmark Descriptions, vol.B, 2018.

H. Barbosa, J. C. Blanchette, M. Fleury, and P. Fontaine, Scalable finegrained proofs for formula processing, J. Autom. Reasoning, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01526841

H. Barbosa, J. C. Blanchette, M. Fleury, P. Fontaine, and H. J. Schurr, Better SMT proofs for easier reconstruction, 4th Conference on Artificial Intelligence and Theorem Proving, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02381819

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic et al., Computer Aided Verification-23rd International Conference, vol.6806, pp.171-177, 2011.

R. J. Bayardo and R. Schrag, Using CSP look-back techniques to solve exceptionally hard SAT instances, Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, vol.1118, pp.46-60, 1996.

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

C. Benzmüller, N. Sultana, L. C. Paulson, and F. Theiß, The higherorder prover l e o-II, J. Autom. Reasoning, vol.55, issue.4, pp.389-404, 2015.

U. Berger, A. Lawrence, F. Forsberg, and M. Seisenberger, Extracting verified decision procedures: DPLL and resolution, Log. Meth. Comput. Sci, vol.11, issue.1, 2015.

A. Biere, Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition, vol.2016, pp.44-45, 2016.

A. Biere, . Cadical, . Lingeling, and T. Plingeling, YalSAT entering the SAT Competition, SAT Competition 2017: Solver and Benchmark Descriptions, pp.14-15, 2017.

A. Biere, Deep bound hardware model checking instances, quadratic propagations benchmarks and reencoded factorization problems, pp.37-38, 2017.

A. Biere and A. Fröhlich, Evaluating CDCL variable scoring schemes, Theory and Applications of Satisfiability Testing-SAT 2015-18th International Conference, vol.9340, pp.405-422, 2015.

A. Biere and A. Fröhlich, Evaluating CDCL restart schemes

, Theory and Applications of Satisfiability Testing-SAT 2015-18th International Conference, vol.9340, pp.405-422, 2015.

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

J. C. Blanchette, Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk), Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs-CPP 2019, pp.1-13, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01937136

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic proof and disproof in Isabelle/HOL, Frontiers of Combining Systems, 8th International Symposium, vol.6989, pp.12-27, 2011.

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, 2015.
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.

J. C. Blanchette, M. Fleury, P. Lammich, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality
URL : https://hal.archives-ouvertes.fr/hal-01336074

, J. Autom. Reasoning, vol.61, issue.1-4, pp.333-365, 2018.

J. C. Blanchette, M. Fleury, and D. Traytel, Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL, 2nd International Conference on Formal Structures for Computation and Deduction, vol.84, pp.1-11, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01599176

J. C. Blanchette, M. Fleury, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, vol.9706, pp.25-44, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01336074

J. C. Blanchette, M. Fleury, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, vol.9706, pp.25-44, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01336074

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, Interactive Theorem Proving, First International Conference, ITP 2010, vol.6172, pp.179-194, 2010.

R. Bottesch, M. W. Haslbeck, and R. Thiemann, Verifying an incremental theory solver for linear arithmetic in isabelle/hol, Frontiers of Combining Systems-12th International Symposium, pp.223-239, 2019.

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An open, trustable and efficient SMT-solver, 22nd International Conference on Automated Deduction, vol.5663, pp.151-156, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430634

M. Bromberger, M. Fleury, S. Schwarz, and C. Weidenbach, SPASS-SATT a CDCL(LA) solver, Automated Deduction-CADE 27-27th International Conference on Automated Deduction, pp.111-122, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405524

C. E. Brown, Satallax: An automatic higher-order prover, Automated Reasoning-6th International Joint Conference, IJCAR 2012, vol.7364, pp.111-117, 2012.

R. E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler, COS-MOS: A compiled simulator for MOS circuits, 24th ACM/IEEE conference proceedings on Design automation conference-DAC '87, pp.9-16, 1987.

L. Bulwahn, A. Krauss, F. Haftmann, L. Erkök, and J. Matthews, Imperative functional programming with Isabelle/HOL, Theorem Proving in Higher Order Logics, 21st International Conference, vol.5170, pp.134-149, 2008.

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional programming-ICFP '11, pp.418-430, 2011.

M. S. Chowdhury, M. Müller, and J. You, Characterization of glue variables in CDCL SAT solving, 2019.

G. Chu, A. Harwood, and P. J. Stuckey, Cache conscious data structures for Boolean satisfiability solvers, JSAT, vol.6, issue.1-3, pp.99-120, 2009.

A. Church, A formulation of the simple theory of types, J. symb. log, vol.5, issue.02, pp.56-68, 1940.

M. Clochard, J. Filliâtre, and A. Paskevich, How to avoid proving the absence of integer overflows, Verified Software: Theories, Tools, and Experiments-7th International Conference, vol.9593, pp.94-109, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01162661

L. Cruz-filipe, M. J. Heule, W. A. Hunt, M. Kaufmann, and P. Schneider-kamp, Efficient certified RAT verification, Automated Deduction-CADE 26-26th International Conference on Automated Deduction, vol.10395, pp.220-236, 2017.

L. Cruz-filipe, J. P. Marques-silva, and P. Schneider-kamp, Efficient certified resolution proof checking, Tools and Algorithms for the Construction and Analysis of Systems-23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10205, pp.118-135, 2017.

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving

, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

B. Delaware, C. Pit-claudel, J. Gross, and A. Chlipala, Fiat: Deductive synthesis of abstract data types in a proof assistant, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages-POPL '15, pp.689-700, 2015.

N. Eén and N. Sörensson, An extensible SAT-solver, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, vol.2919, pp.502-518, 2003.

J. Elffers and J. Nordström, Visualizing CDCL VSIDS and phase values, Workshop on the Pragmatics of SAT 2019, held as part of Theory and Applications of Satisfiability Testing-SAT 2019, 2019.

J. Filliâtre and A. Paskevich, Why3-where programs meet provers, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, pp.125-128, 2013.

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

M. Sc and . Thesis, , 2015.

M. Fleury, Optimizing a verified SAT solver, NASA Formal Methods-11th International Symposium, NFM 2019, vol.11460, pp.148-165, 2019.

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

, Formal proof development

M. Fleury, J. C. Blanchette, and P. Lammich, A verified SAT solver with watched literals using Imperative HOL, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs-CPP 2018, pp.158-171, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01904647

M. Fleury and H. J. Schurr, Reconstructing veriT proofs in Isabelle/HOL, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, pp.36-50, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02276530

A. V. Gelder, Improved conflict-clause minimization leads to improved propositional proof traces, Theory and Applications of Satisfiability Testing-SAT 2009, 12th International Conference, vol.5584, pp.141-146, 2009.

I. P. Gent, Optimal implementation of watched literals and more general techniques

, J. Artif. Intell. Res, vol.48, pp.231-252, 2013.

E. Giunchiglia and M. Maratea, Including Prestigious Applications of Intelligent Systems, Proceedings, Frontiers in Artificial Intelligence and Applications, vol.141, pp.377-381, 2006.

M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF, vol.78, 1979.

D. Gries and D. M. Volpano, The Transform-A new language construct, Structured Programming, vol.11, issue.1, pp.1-10, 1990.

F. Haftmann, Draft toy for proof exploration, 2013.

F. Haftmann and T. Nipkow, Code generation via higher-order rewrite systems, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, vol.6009, pp.103-117, 2010.

J. Harrison, Formalizing basic first order model theory, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, vol.1479, pp.153-170, 1998.

M. J. Heule, Open source development, pp.2019-2022, 2014.

M. J. Heule, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), pp.6598-6606, 2018.

M. J. Heule, W. A. Hunt, and N. Wetzler, Trimming while checking clausal proofs

, Computer-Aided Design (FMCAD), vol.10499, pp.269-284, 2013.

M. J. Heule, W. A. Hunt, and N. Wetzler, Bridging the gap between easy generation and efficient verification of unsatisfiability proofs, Softw. Test. Verif. Reliab, vol.24, issue.8, pp.593-607, 2014.

M. J. Heule, O. Kullmann, and V. W. Marek, Solving very hard problems: Cube-and-conquer, a hybrid SAT solving method, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, vol.9710, pp.228-245, 2017.

L. Hupel, Verified code generation from Isabelle/HOL, TUM, 2019.

L. Hupel and T. Nipkow, A verified compiler from Isabelle/HOL to CakeML, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10801, pp.999-1026, 2018.

A. B. Jensen, J. B. Larsen, A. Schlichtkrull, and J. Villadsen, Programming and verifying a declarative first-order prover in Isabelle/HOL, AI Commun, vol.31, issue.3, pp.281-299, 2018.

F. Kammüller, M. Wenzel, and L. C. Paulson, Locales-A sectioning concept for Isabelle, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, vol.1690, pp.149-166, 1999.

R. M. Karp, Reducibility among combinatorial problems, Proceedings of a symposium on the Complexity of Computer Computations, pp.85-103, 1972.

G. Klein, M. Norrish, T. Sewell, H. Tuch, S. Winwood et al., seL4: Formal verification of an operating-system kernel, Commun. ACM, vol.53, issue.6, p.107, 2010.

A. Krauss, Partial recursive functions in higher-order logic, Automated Reasoning, Third International Joint Conference, vol.4130, pp.589-603, 2006.

S. Krsti? and A. Goel, Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL, Frontiers of Combining Systems, 6th International Symposium, vol.4720, pp.1-27, 2007.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: a verified implementation of ml, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages-POPL '14, vol.10900, pp.646-662, 2014.

P. Lammich, Interactive Theorem Proving-6th International Conference, Proceedings, vol.9236, pp.253-269, 2015.

P. Lammich, Refinement based verification of imperative data structures, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs-CPP 2016, vol.7998, pp.84-99, 2016.

P. Lammich, Refinement based verification of imperative data structures, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs-CPP 2016, pp.27-36, 2016.

P. Lammich, Efficient verified (UN)SAT certificate checking, Automated Deduction-CADE 26-26th International Conference on Automated Deduction, vol.10395, pp.237-254, 2017.

P. Lammich, The GRAT tool chain-efficient (UN)SAT certificate checking with formal correctness guarantees, Theory and Applications of Satisfiability Testing-SAT 2017-20th International Conference, vol.10491, pp.457-463, 2017.

P. Lammich, Generating verified LLVM from Isabelle/HOL, 10th International Conference on Interactive Theorem Proving, ITP 2019, vol.141, pp.1-22, 2019.

J. Larrosa, R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-carbonell, A framework for certified boolean branch-and-bound optimization, J. Autom. Reasoning, vol.46, issue.1, pp.81-102, 2010.

C. Lattner and V. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, pp.75-88, 2004.

K. R. Leino, Dafny: An automatic program verifier for functional correctness, Logic for Programming, Artificial Intelligence, and Reasoning-16th International Conference, LPAR-16, vol.6355, pp.348-370, 2010.

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. Theses, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

C. Li and F. Manyà, MaxSAT, hard and soft constraints, Handbook of Satisfiability, vol.185, pp.613-631, 2009.

C. Li, F. Xiao, M. Luo, F. Manyà, Z. Lü et al., Clause vivification by unit propagation in CDCL SAT solvers, 2018.

J. H. Liang, V. Ganesh, E. Zulkoski, A. Zaman, and K. Czarnecki, Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers, Hardware and Software: Verification and Testing-11th International Haifa Verification Conference, vol.9434, pp.225-241, 2015.

P. Liberatore, Algorithms and experiments on finding minimal models, Dipartimento di Informatica e Sistemistica, 1999.

A. Lochbihler, Fast machine words in Isabelle/HOL. In: Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, pp.388-410, 2018.

M. Luby, A. Sinclair, and D. Zuckerman, Optimal speedup of Las Vegas algorithms, Information Processing Letters, vol.47, issue.4, pp.90029-90038, 1993.

M. Luo, C. M. Li, F. Xiao, F. Manyà, and Z. Lü, An effective learnt clause minimization approach for CDCL SAT solvers, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, pp.703-711, 2017.

Y. S. Mahajan, Z. Fu, and S. Malik, zChaff 2004: An efficient SAT solver, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, vol.3542, pp.360-375, 2004.

V. Manquinho and J. P. Marques-silva, Satisfiability-based algorithms for pseudo-boolean optimization using gomory cuts and search restarts, 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'05), pp.150-155, 2005.

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

F. Mari?, Formal verification of modern SAT solvers. Archive of Formal Proofs, 2008.

F. Mari?, Formalization and implementation of modern SAT solvers, J. Autom. Reasoning, vol.43, issue.1, pp.81-119, 2009.

F. Mari?, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theoretical Computer Science, vol.411, issue.50, pp.4333-4356, 2010.

F. Mari? and P. Jani?i?, Formalization of abstract state transition systems for SAT, Log.Meth.Comput.Sci, vol.7, issue.3, 2011.

J. P. Marques-silva, Workshop on the Pragmatics of SAT 2019, held as part of Theory and Applications of Satisfiability Testing-SAT 2019, 2019.

M. Silva, J. P. Sakallah, and K. , GRASP-a new search algorithm for satisfiability, Proceedings of International Conference on Computer Aided Design, pp.220-227, 1996.

D. Matichuk, T. Murray, and M. Wenzel, Eisbach: A proof method language for Isabelle, J. Autom. Reasoning, vol.56, issue.3, pp.261-282, 2016.

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

S. Möhle and A. Biere, Backing backtracking, Theory and Applications of Satisfiability Testing-SAT 2019-22nd International Conference, SAT 2019, vol.11628, pp.250-266, 2019.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation-DAC '01, pp.530-535, 2001.

L. M. De-moura and N. Bjørner, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.4963, pp.337-340, 2008.

A. Nadel and V. Ryvchin, Chronological backtracking, Theory and Applications of Satisfiability Testing-SAT 2018-21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC, vol.10929, pp.111-121, 2018.

D. E. Narváez, Formalizing CNF SAT symmetry breaking in PVS, NASA Formal Methods-11th International Symposium, NFM 2019, vol.11460, pp.341-354, 2019.

Z. Newsham, V. Ganesh, S. Fischmeister, G. Audemard, and L. Simon, Impact of community structure on SAT solver performance, Theory and Applications of Satisfiability Testing-SAT 2014-17th International Conference, Held as Part of the Vienna Summer of Logic, vol.8561, pp.252-268, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00994301

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

T. Nipkow and G. Klein, Concrete Semantics, 2014.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science

, , 2002.

P. A. Noel, Experimenting with Isabelle in ZF set theory, J. Autom. Reasoning, vol.10, issue.1, pp.15-58, 1993.

L. Noschinski, C. Rizkallah, and K. Mehlhorn, Verification of certifying computations through AutoCorres and Simpl, NASA Formal Methods-6th International Symposium, NFM 2014, vol.8430, pp.46-61, 2014.

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

S. Owre, J. M. Rushby, and N. Shankar, Automated Deduction-CADE-11, 11th International Conference on Automated Deduction, Proceedings, pp.748-752, 1992.

L. Palopoli, F. Pirri, and C. Pizzuti, Algorithms for selective enumeration of prime implicants

, Artif. Intell, vol.111, issue.1-2, pp.41-72, 1999.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, vol.9, pp.1-10, 2010.

N. Peltier, A variant of the superposition calculus. Archive of Formal Proofs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01383903

H. H. Persson, Constructive completeness of intuitionistic predicate logic, 1996.

C. Piette, Y. Hamadi, and L. Sais, Vivifying propositional clausal formulae, Proceedings, Frontiers in Artificial Intelligence and Applications, vol.178, pp.525-529, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00865274

K. Pipatsrisawat and A. Darwiche, A lightweight component caching scheme for satisfiability solvers, Theory and Applications of Satisfiability Testing-SAT 2007, 10th International Conference, vol.4501, pp.294-299, 2007.

A. Ramos, P. Van-der-tak, and M. J. Heule, Between restarts and backjumps, Theory and Applications of Satisfiability Testing-SAT 2011-14th International Conference, SAT 2011, vol.6695, pp.216-229, 2011.

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.

A. Riazanov and A. Voronkov, The design and implementation of VAM-PIRE, AI Commun, vol.15, issue.2-3, pp.91-110, 2002.

K. Roe and S. F. Smith, Using the coq theorem prover to verify complex data structure invariants, 2018.

L. Ryan, Efficient algorithms for clause-learning SAT solvers, 2004.

A. Schlichtkrull, Formalization of the resolution calculus for first-order logic, Interactive Theorem Proving-7th International Conference, vol.9807, pp.341-357, 2016.

A. Schlichtkrull, J. C. Blanchette, and D. Traytel, A verified functional implementation of Bachmair and Ganzinger's ordered resolution prover. Archive of Formal Proofs, 2018.

A. Schlichtkrull, J. C. Blanchette, and D. Traytel, A verified prover based on ordered resolution, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.152-165, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01937141

A. Schlichtkrull, J. C. Blanchette, D. Traytel, and U. Waldmann, Formalizing Bachmair and Ganzinger's ordered resolution prover, Automated Reasoning-9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, vol.10900, pp.89-107, 2018.

S. Schulz, E-a brainiac theorem prover, AI Commun, vol.15, issue.2

R. Sebastiani, P. Giorgini, and J. Mylopoulos, Advanced Information Systems Engineering, 16th International Conference, Proceedings, Lecture Notes in Computer Science, vol.3084, pp.20-35, 2004.

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

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

M. Soos, K. Nohl, and C. Castelluccia, Extending SAT solvers to cryptographic problems, Lecture Notes in Computer Science, vol.5584, pp.244-257

H. Springer-berlin, , 2009.

N. Sörensson and A. Biere, Minimizing learned clauses, Theory and Applications of Satisfiability Testing-SAT 2009, 12th International Conference, vol.5584, pp.237-243, 2009.

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

A. Stump, M. Deters, A. Petcher, T. Schiller, and T. Simpson, Verified programming in guru, Proceedings of the 3rd workshop on Programming languages meets program verification-PLPV '09, pp.49-58, 2008.

R. Thiemann, Extending a verified simplex algorithm, LPAR-22 Workshop and Short Paper Proceedings, vol.9, pp.37-48, 2018.

A. Voronkov, AVATAR: The architecture for first-order theorem provers, Computer Aided Verification-26th International Conference, vol.8559, pp.696-710, 2014.

S. Weeks, Whole-program compilation in MLton, Proceedings of the ACM Workshop on ML, p.1, 2006.

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

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., Automated Deduction-CADE-22, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009.

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.

M. Wenzel, Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, vol.167, pp.84-94, 2014.

M. Wenzel, Further scaling of Isabelle technology, p.2018, 2018.

N. Wetzler, M. J. Heule, and W. A. Hunt, DRAT-trim: Efficient checking and trimming using expressive clausal proofs, Theory and Applications of Satisfiability Testing-SAT 2014-17th International Conference, Held as Part of the Vienna Summer of Logic, vol.8561, pp.422-429, 2014.

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

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

L. Yu, A formal model of IEEE floating point arithmetic. Archive of Formal Proofs, 2013.

, Formal proof development

H. Zhang, SATO: an efficient propositional prover, 14th International Conference on Automated Deduction, vol.1249, pp.272-275, 1997.