R. Atkey and C. Mcbride, Productive coprogramming with guarded recursion, ICFP '13, pp.197-208, 2013.

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

P. Baumgartner and J. Bax, Proving Infinite Satisfiability, LPAR-19, pp.86-95, 2013.
DOI : 10.1007/978-3-642-45221-5_6

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, Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions, Software Quality Journal, vol.20, issue.1, pp.101-126, 2013.
DOI : 10.1007/s11219-011-9148-5

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Autom. Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette and A. Krauss, Monotonicity Inference for Higher-Order Formulas, Journal of Automated Reasoning, vol.178, issue.1, pp.369-398, 2011.
DOI : 10.1007/s10817-011-9234-1

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

J. C. Blanchette, A. Popescu, and D. Traytel, Foundational extensible corecursion: A proof assistant perspective, p.15, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01212589

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

K. Claessen, A. Lillieström, and N. Smallbone, Sort It Out with Monotonicity, LNCS, vol.5, issue.2, pp.207-221, 2011.
DOI : 10.1007/BF00243005

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, Relevancy propagation, 2007.

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.

J. A. Goguen and R. M. Burstall, Institutions: abstract model theory for specification and programming, Journal of the ACM, vol.39, issue.1, pp.95-146, 1992.
DOI : 10.1145/147508.147524

D. Jackson, Nitpick: A checkable specification language, FMSP '96, pp.60-69, 1996.

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.

F. Lindblad, Property directed generation of first-order test data, Intellect, pp.105-123, 2007.

W. Mccune, Prover9 and Mace4

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

A. J. Reynolds, Finite Model Finding in Satisfiability Modulo Theories, 2013.

C. Runciman, M. Naylor, and F. Lindblad, SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values, pp.37-48, 2008.

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

D. A. Turner, Elementary strong functional programming, FPLE '95, pp.1-13, 1995.
DOI : 10.1007/3-540-60675-0_35

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.