L. Bachmair and &. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, I, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450

P. Baumgartner and A. Fuchs, 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

Y. Bertot and &. Pierre-castéran, Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, 2004.
DOI : 10.1007/978-3-662-07964-5

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

C. Jasmin and . Blanchette, Automatic Proofs and Refutations for Higher-Order Logic, 2012.

C. Jasmin and . Blanchette, Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions, Softw. Qual. J, vol.21, issue.1, pp.101-12610, 2013.

J. Christian-blanchette, C. Kaliszyk, L. C. Paulson, and &. Urban, Hammering towards QED, J. Formal. Reasoning, vol.9, issue.1, pp.101-148, 2016.

J. Nipkow, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, ITP 2010, pp.131-146, 2010.

L. Bulwahn, The New Quickcheck for Isabelle, CPP 2012, pp.92-108, 2012.
DOI : 10.1007/978-3-642-35308-6_10

R. Caferra, A. Leitsch, and &. Peltier, Automated Model Building Applied Logic 31, 2004.

M. Carlier, C. Dubois, and &. Gotlieb, A First Step in the Design of a Formally Verified Constraint-Based Testing Tool: FocalTest, TAP 2012, pp.35-50, 2012.
DOI : 10.1007/978-3-642-30473-6_5

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

A. Chaieb and &. Nipkow, Proof Synthesis and Reflection for Linear Arithmetic, Journal of Automated Reasoning, vol.10, issue.5, pp.33-5910, 2008.
DOI : 10.1007/s10817-008-9101-x

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.304.7968

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

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

E. M. Clarke and J. , Orna Grumberg & Doron A. Peled (1999): Model Checking

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA???+??? Proofs, FM 2012, pp.147-154, 2012.
DOI : 10.1007/978-3-642-32759-9_14

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

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

P. Dybjer, Q. Haiyan, and &. Takeyama, Combining Testing and Proving in Dependent Type Theory, TPHOLs 2003, pp.188-20310, 2003.
DOI : 10.1007/10930755_12

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6779

W. Guttmann, G. Struth, and &. Weber, Automating Algebraic Methods in Isabelle, ICFEM 2011, pp.617-632, 2011.
DOI : 10.1007/978-94-010-0413-8_11

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

D. Jackson, Software Abstractions: Logic, Language, and Analysis, 2006.

B. Jacobs and &. Tom-melham, Translating dependent type theory into higher order logic, TLCA 1993, pp.209-22910, 1993.
DOI : 10.1007/BFb0037108

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.7356

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.381.657

V. Kuncak and &. Jackson, Relational analysis of algebraic datatypes, pp.207-216, 2005.

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

A. Lochbihler and &. Lukas-bulwahn, Animating the Formalised Semantics of a Java-Like Language, ITP 2011, pp.216-232, 2011.
DOI : 10.1007/978-3-642-03359-9_31

P. Manolios, Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities, ITP 2013, p.18, 2013.
DOI : 10.1007/978-3-642-39634-2_4

W. Mccune, Prover9 and Mace4

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

S. Owre, Random testing in PVS, AFM '06, 2006.

Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, &. Benjamin et al., Foundational Property-Based Testing, ITP 2015, pp.325-343, 2015.
DOI : 10.1007/978-3-319-22102-1_22

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

W. Reif, G. Schellhorn, and A. Thums, Flaw Detection in Formal Specifications, IJCAR 2001, pp.642-657, 2001.
DOI : 10.1007/3-540-45744-5_52

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2528

A. Reynolds and &. Blanchette, A decision procedure for (co)datatypes in SMT solvers, CADE-25, pp.197-213, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01212585

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

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

A. Reynolds, C. Tinelli, and A. Goel, Quantifier Instantiation Techniques for Finite Model Finding in SMT, LNCS, vol.7898, pp.24-377, 2013.
DOI : 10.1007/978-3-642-38574-2_26

C. Runciman, M. Naylor, and &. Lindblad, SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values, pp.37-4810, 2008.
DOI : 10.1145/1543134.1411292

K. John and . Slaney, FINDER: Finite domain enumerator?System description, LNCS, vol.814, pp.12-798, 1994.

M. Sozeau and &. Oury, First-Class Type Classes, TPHOLs 2008, pp.278-293, 2008.
DOI : 10.1007/11542384_8

URL : https://hal.archives-ouvertes.fr/inria-00628864

P. Suter and A. Viktor-kuncak, Satisfiability Modulo Recursive Programs, SAS 2011, pp.298-315, 2011.
DOI : 10.1007/978-3-540-77395-5_17

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.697.8573

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

M. Wenzel, Type classes and overloading in higher-order logic, TPHOLs 1997, pp.307-32210, 1997.
DOI : 10.1007/BFb0028402

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.782

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