Concolic Execution and Test Case Generation in Prolog

  • Germán VidalEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)


Symbolic execution extends concrete execution by allowing symbolic input data and then exploring all feasible execution paths. It has been defined and used in the context of many different programming languages and paradigms. A symbolic execution engine is at the heart of many program analysis and transformation techniques, like partial evaluation, test case generation or model checking, to name a few. Despite its relevance, traditional symbolic execution also suffers from several drawbacks. For instance, the search space is usually huge (often infinite) even for the simplest programs. Also, symbolic execution generally computes an overapproximation of the concrete execution space, so that false positives may occur. In this paper, we propose the use of a variant of symbolic execution, called concolic execution, for test case generation in Prolog. Our technique aims at full statement coverage. We argue that this technique computes an underapproximation of the concrete execution space (thus avoiding false positives) and scales up better to medium and large Prolog applications.


Execution Path Symbolic Execution Test Case Generation Symbolic State Program Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The author gratefully acknowledges the anonymous referees and the participants of LOPSTR 2014 for many useful comments and suggestions. I would also like to thank Fred Mesnard and Etienne Payet for their remarks to improve the paper.


  1. 1.
    Albert, E., Arenas, P., Gómez-Zamalloa, M., Rojas, J.M.: Test case generation by symbolic execution: basic concepts, a CLP-based instance, and actor-based concurrency. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 263–309. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  2. 2.
    Belli, F., Jack, O.: Implementation-based analysis and testing of Prolog programs. In: ISSTA, pp. 70–80. ACM (1993)Google Scholar
  3. 3.
    Clarke, L.A.: A program testing system. In: Proceedings of the 1976 Annual Conference (ACM’76), Houston, pp. 488–491 (1976)Google Scholar
  4. 4.
    De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive partial deduction: foundations, control, algorithms, and experiments. J. Log. Program. 41(2&3), 231–277 (1999)Google Scholar
  5. 5.
    Giesl, J., Ströder, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs. In: PPDP’12, pp. 1–12. ACM (2012)Google Scholar
  6. 6.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI’05, pp. 213–223. ACM (2005)Google Scholar
  7. 7.
    Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012)CrossRefGoogle Scholar
  8. 8.
    Gómez-Zamalloa, M., Albert, E., Puebla, G.: Test case generation for object-oriented imperative languages in CLP. TPLP 10(4–6), 659–674 (2010)zbMATHGoogle Scholar
  9. 9.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefzbMATHGoogle Scholar
  10. 10.
    Leuschel, M.: The DPPD (Dozens of Problems for Partial Deduction) Library of Benchmarks. (2007)
  11. 11.
    Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)Google Scholar
  12. 12.
    Lloyd, J.W., Shepherdson, J.C.: Partial evaluation in logic programming. J. Log. Program. 11, 217–242 (1991)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Martens, B., Gallagher, J.: Ensuring global termination of partial deduction while allowing flexible polyvariance. In: Proceedings of ICLP’95, pp. 597–611. MIT Press (1995)Google Scholar
  14. 14.
    Pasareanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: Pecheur, C., Andrews, J., Di Nitto, E. (eds.) ASE, pp. 179–180. ACM (2010)Google Scholar
  15. 15.
    Rojas, J.M., Gómez-Zamalloa, M.: A framework for guided test case generation in constraint logic programming. In: Albert, E. (ed.) Proceedings of LOPSTR. LNCS, vol. 7844, pp. 176–193. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  16. 16.
    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/SIGSOFT FSE 2005, pp. 263–272. ACM (2005)Google Scholar
  17. 17.
    Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., Fuhs, C.: A linear operational semantics for termination and complexity analysis of \(\sf ISO\) \(\sf Prolog\). In: Vidal, G. (ed.) LOPSTR’11. LNCS, vol. 7225, pp. 237–252. Springer, Heidelberg (2012) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.MiST, DSICUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations