. Barrett, An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007.

. Barrett, Extending Sledgehammer with SMT solvers, Computer Aided Verification, pp.171-177, 2011.

. Ge and . De-moura, Yeting Ge and Leonardo de Moura Complete instantiation for quantified formulas in satisfiability modulo theories, Computer Aided Verification, pp.306-320, 2009.

L. Xavier, [Lochbihler, 2014] Andreas Lochbihler Making the Java memory model safe, Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis?Putnam?Logemann?Loveland procedure to DPLL(T ). J. ACM, pp.363-4461, 2006.

B. Reynolds, A. Reynolds, and J. C. Blanchette, A decision procedure for (co)datatypes in SMT solvers, Conference on Automated Deduction, pp.197-213
URL : https://hal.archives-ouvertes.fr/hal-01212585