S. Antoy, R. Echahed, and M. Hanus, A Needed Narrowing Strategy, Journal of the ACM (JACM), 2000.
DOI : 10.1145/174675.177899
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.8711

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard Version 2.6, 2016.
DOI : 10.1007/978-3-642-19583-9_2

C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Splitting on Demand in SAT Modulo Theories, International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp.512-526, 2006.
DOI : 10.1007/11916277_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.406.7657

C. Barrett, I. Shikanian, and C. Tinelli, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Electronic Notes in Theoretical Computer Science, vol.174, issue.8, pp.23-37, 2007.
DOI : 10.1016/j.entcs.2006.11.037

K. Claessen and J. Hughes, QuickCheck, ACM SIGPLAN Notices, vol.46, issue.4, pp.53-64, 2011.
DOI : 10.1145/1988042.1988046

K. Claessen, M. Johansson, D. Rosén, and N. Smallbone, TIP: Tons of Inductive Problems, Conferences on Intelligent Computer Mathematics, pp.333-337, 2015.
DOI : 10.1007/978-3-642-28756-5_28
URL : http://publications.lib.chalmers.se/records/fulltext/222739/local_222739.pdf

K. Claessen and D. Rosén, SAT-based Bounded Model Checking for Functional Programs. https://github, p.2016

S. Cruanes and J. C. Blanchette, Extending Nunchaku to Dependent Type Theory, Proceedings First International Workshop on Hammers for Type Theories, pp.3-12, 2016.
DOI : 10.4204/EPTCS.210.3
URL : https://hal.archives-ouvertes.fr/hal-01401696

J. Duregård, P. Jansson, and M. Wang, Feat, ACM SIGPLAN Notices, vol.47, issue.12, pp.61-72, 2013.
DOI : 10.1145/2430532.2364515

M. Hanus, A unified computation model for functional and logic programming, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, 1997.
DOI : 10.1145/263699.263710
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.8257

M. Kaufmann and J. Strother-moore, ACL2: an industrial strength version of Nqthm, Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96, pp.23-34, 1996.
DOI : 10.1109/CMPASS.1996.507872
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.7444

E. Richard and . Korf, Depth-first iterative-deepening: An optimal admissible tree search, Artificial intelligence, vol.27, issue.1, pp.97-109, 1985.

F. Lindblad, Property directed generation of first-order test data, Trends in Functional Programming, pp.105-123, 2007.

C. Lawrence and . Paulson, Isabelle: A generic theorem prover, 1994.

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

A. Reynolds, J. C. Blanchette, S. Cruanes, and C. Tinelli, Model Finding for Recursive Functions in SMT, Automated Reasoning -8th International Joint Conference, IJCAR 2016 Proceedings, volume 9706 of Lecture Notes in Computer Science, pp.133-151, 2016.
DOI : 10.1007/3-540-60675-0_35
URL : https://hal.archives-ouvertes.fr/hal-01336082

C. Runciman, M. Naylor, and F. Lindblad, Smallcheck and lazy smallcheck: automatic exhaustive testing for small values, Acm sigplan notices, pp.37-48, 2008.
DOI : 10.1145/1543134.1411292

P. Suter, A. S. Köksal, and V. Kuncak, Satisfiability Modulo Recursive Programs, International Static Analysis Symposium, pp.298-315, 2011.
DOI : 10.1007/978-3-540-77395-5_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.233.6117