C. Ballarin, Locales: A Module System for Mathematical Theories, Journal of Automated Reasoning, vol.254, issue.2, pp.123-153, 2014.
DOI : 10.1007/s10817-013-9284-7

B. Jr, R. J. Schrag, and R. , Using CSP look-back techniques to solve exceptionally hard SAT instances, ) CP96. LNCS, pp.46-60, 1996.

J. C. Blanchette, M. Fleury, and C. Weidenbach, A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality, IJCAR 2016, 2016.
DOI : 10.1007/978-3-319-23506-6_12
URL : https://hal.archives-ouvertes.fr/hal-01401807

J. C. Blanchette, M. Fleury, A. Schlichtkrull, and D. Traytel, IsaFoL: Isabelle Formalization of Logic

M. Davis, G. Logemann, and D. W. 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. Fleury and J. C. Blanchette, Formalization of Weidenbach's Automated Reasoning?The Art of Generic Problem Solving

M. Heule, H. Jr, W. A. Wetzler, and N. , Bridging the gap between easy generation and efficient verification of unsatisfiability proofs, Software Testing, Verification and Reliability, vol.411, issue.50, pp.593-607, 2014.
DOI : 10.1002/stvr.1549

F. Kammüller, M. Wenzel, and L. C. Paulson, Locales A Sectioning Concept for Isabelle, TPHOLs '99, pp.149-166, 1999.
DOI : 10.1007/3-540-48256-3_11

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, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

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

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, pp.696-710, 2014.
DOI : 10.1007/978-3-319-08867-9_46

C. Weidenbach, Automated Reasoning Building Blocks, Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp.172-188, 2015.
DOI : 10.1007/978-3-319-23506-6_12
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, Studies in Logic, Grammar, and Rhetoric, 2007.