C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB standard?Version 2.5, 2015.

P. Baumgartner, A. Fuchs, H. De-nivelle, and C. Tinelli, Computing finite models by reduction to function-free clause logic, Journal of Applied Logic, vol.7, issue.1, pp.58-74, 2009.
DOI : 10.1016/j.jal.2007.07.005

R. Blanc, V. Kuncak, E. Kneuss, and P. Suter, An overview of the Leon verification system? Verification by translation to recursive functions, Scala '13, 2013.

J. C. Blanchette and T. Nipkow, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, LNCS, vol.6172, pp.131-146, 2010.
DOI : 10.1007/978-3-642-14052-5_11

K. Claessen and J. Hughes, QuickCheck: A lightweight tool for random testing of Haskell programs, ICFP '00, pp.268-279, 2000.

K. Claessen and N. Sörensson, New techniques that improve MACE-style model finding, MODEL, 2003.

L. De-moura and N. Bjørner, Efficient E-Matching for SMT Solvers, LNCS, vol.4603, pp.21-183, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, LNCS, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

A. Dunets, G. Schellhorn, and W. Reif, Automated Flaw Detection in Algebraic Specifications, Journal of Automated Reasoning, vol.20, issue.1, pp.359-395, 2010.
DOI : 10.1007/s10817-010-9166-1

Y. Ge and L. De-moura, Complete instantiation for quantified formulas in satisfiability modulo theories, CAV '09, pp.306-320, 2009.

M. Johansson, L. Dixon, and A. Bundy, Case-Analysis for Rippling and Inductive Proof, ITP 2010, pp.291-306, 2010.
DOI : 10.1007/978-3-642-14052-5_21

K. Korovin, Non-cyclic Sorts for First-Order Satisfiability, FroCoS 2013, pp.214-228, 2013.
DOI : 10.1007/978-3-642-40885-4_15

A. Krauss, Automating Recursive Definitions and Termination Proofs in Higher-Order Logic, 2009.

V. Kuncak and D. Jackson, Relational analysis of algebraic datatypes, 2005.

W. Mccune, A Davis?Putnam program and its application to finite first-order model search: Quasigroup existence problems, 1994.

A. Reynolds and J. C. Blanchette, A decision procedure for (co)datatypes in SMT solvers, LNCS, p.25, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01212585

A. Reynolds, J. C. Blanchette, and C. Tinelli, Model Finding for Recursive Functions in SMT, 2015.
DOI : 10.1007/978-3-319-40229-1_10

URL : https://hal.archives-ouvertes.fr/hal-01242509

A. Reynolds and V. Kuncak, Induction for SMT Solvers, VMCAI 2015, pp.80-98, 2014.
DOI : 10.1007/978-3-662-46081-8_5

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

A. Reynolds, C. Tinelli, A. Goel, and S. Krsti´ckrsti´c, Finite Model Finding in SMT, CAV 2013, pp.640-655, 2013.
DOI : 10.1007/978-3-642-39799-8_42

A. Reynolds, C. Tinelli, A. Goel, S. Krsti´ckrsti´c, M. Deters et al., Quantifier Instantiation Techniques for Finite Model Finding in SMT, LNCS, vol.7898, issue.24, pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26

J. K. Slaney, FINDER: Finite domain enumerator system description, LNCS, vol.814, issue.12, pp.798-801, 1994.
DOI : 10.1007/3-540-58156-1_63

E. Torlak and D. Jackson, Kodkod: A Relational Model Finder, TACAS 2007, pp.632-647, 2007.
DOI : 10.1007/978-3-540-71209-1_49

T. Weber, SAT-Based Finite Model Generation for Higher-Order Logic, 2008.

J. Zhang and H. Zhang, SEM: A system for enumerating models, IJCAI- 95, pp.298-303, 1995.