Concolic Execution and Test Case Generation in Prolog
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.
KeywordsExecution Path Symbolic Execution Test Case Generation Symbolic State Program Clause
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.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.Belli, F., Jack, O.: Implementation-based analysis and testing of Prolog programs. In: ISSTA, pp. 70–80. ACM (1993)Google Scholar
- 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.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.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.Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI’05, pp. 213–223. ACM (2005)Google Scholar
- 10.Leuschel, M.: The DPPD (Dozens of Problems for Partial Deduction) Library of Benchmarks. http://www.ecs.soton.ac.uk/mal/systems/dppd.html (2007)
- 11.Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)Google Scholar
- 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.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
- 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