An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007. ,
Extending Sledgehammer with SMT solvers, Computer Aided Verification, pp.171-177, 2011. ,
Yeting Ge and Leonardo de Moura Complete instantiation for quantified formulas in satisfiability modulo theories, Computer Aided Verification, pp.306-320, 2009. ,
[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. ,
A decision procedure for (co)datatypes in SMT solvers, Conference on Automated Deduction, pp.197-213 ,
URL : https://hal.archives-ouvertes.fr/hal-01212585