E. Albert, P. Arenas, M. Gómez-zamalloa, and J. Rojas, Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency, SFM 2014, vol.8483, pp.263-309, 2014.

K. Apt, From Logic Programming to Prolog, 1997.

F. Belli and O. Jack, Implementation-based analysis and testing of Prolog programs, ISSTA, pp.70-80, 1993.

M. Carlsson and P. Mildner, SICStus Prolog-the first 25 years, Theory and Practice of Logic Programming, vol.12, pp.35-66, 2012.

K. Claessen and J. Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proc. of (ICFP, pp.268-279, 2000.

L. Clarke, A program testing system, Proceedings of the 1976 Annual Conference (ACM'76), pp.488-491, 1976.

F. Degrave, T. Schrijvers, and W. Vanhoof, Automatic generation of test inputs for Mercury, Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR, pp.71-86, 2008.

P. Godefroid, N. Klarlund, and K. Sen, DART: directed automated random testing, Proc. of PLDI'05, pp.213-223, 2005.

P. Godefroid, M. Levin, and D. Molnar, Sage: whitebox fuzzing for security testing, CACM, vol.55, pp.40-44, 2012.

M. Gómez-zamalloa, E. Albert, and G. Puebla, Test case generation for object-oriented imperative languages in CLP, TPLP, vol.10, pp.659-674, 2010.

M. V. Hermenegildo, F. Bueno, M. Carro, P. López-garcía, E. Mera et al., An overview of Ciao and its design philosophy, TPLP, vol.12, pp.219-252, 2012.

J. C. King, Symbolic execution and program testing, CACM, vol.19, pp.385-394, 1976.

J. Lloyd, Foundations of Logic Programming, 1987.

A. Martelli and U. Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, vol.4, pp.258-282, 1982.

E. Mera, P. López-garcía, and M. V. Hermenegildo, Integrating software testing and run-time checking in an assertion verification framework, 25th International Conference on Logic Programming, pp.281-295, 2009.

C. Pasareanu and N. Rungta, Symbolic PathFinder: symbolic execution of Java bytecode, pp.179-180, 2010.

G. Plotkin, A note on inductive generalization, Machine intelligence, vol.5, pp.153-163, 1970.

J. Schimpf and K. Shen, ECL i PS e-from LP to CLP, Theory and Practice of Logic Programming, vol.12, pp.127-156, 2012.

K. Sen, D. Marinov, A. , and G. , CUTE: a concolic unit testing engine for C, Proc. of ESEC/SIGSOFT FSE 2005, pp.263-272, 2005.

Z. Somogyi, F. Henderson, C. , and T. , The execution algorithm of Mercury, an efficient purely declarative Logic Programming language, The Journal of Logic Programming, vol.29, pp.17-64, 1996.

T. Ströder, F. Emmes, P. Schneider-kamp, J. Giesl, and C. Fuhs, A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog, LOPSTR'11, vol.7225, pp.237-252, 2011.

T. Vasak and J. Potter, Characterization of terminating logic programs, Proc. of the, pp.140-147, 1986.

G. Vidal, Concolic Execution and Test Case Generation in Prolog, Proc. of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'14, vol.8981, pp.167-181, 2015.

J. Wielemaker, T. Schrijvers, M. Triska, and T. Lager, SWI-Prolog, Theory and Practice of Logic Programming, vol.12, pp.67-96, 2012.

F. , Payet and G. Vidal Example, vol.7

Y. Let-a-=-p(x and H. , p(a, a), p(b, b)}. Then the loop at line 2 considers the simple disagreement pairs in B and, for instance, it sets B to {p(a, a), p(b, b)} (it may also set B to {p(a, b), p(a, a), p(b, b)} or to {p(b, a), p(a, a), p(b, b)}). As no simple disagreement pair now occurs in B, the algorithm jumps at line 3. The pair a, b occurs twice in A. Action (3b) replaces each occurrence with the same variable U ? U, p(b, b)}. First the algorithm sets B := {p(X, Y )

Y. Let-a-=-p(x and H. , p(a, b), p(b, a)}. Then the loop at line 2 considers the simple disagreement pairs in B and, for instance, it sets B to {p(a, b), p(b, a)} (it may also set B to {p(a, a), p(a, b), p(b, a)} or to {p(b, b), p(a, b), p(b, a)}). As no simple disagreement pair now occurs in B, the algorithm jumps at line 3. The pairs a, b and b, a occur once in A and Action (3b) replaces them with two different variables U, U ? ? U, First the algorithm sets B := {p(X, Y )