Concolic Testing in Logic programming

Software testing is one of the most popular validation techniques in the software industry. Surprisingly, we can only find a few approaches to testing in the context of logic programming. In this paper, we introduce a systematic approach for dynamic testing that combines both concrete and symbolic execution. Our approach is fully automatic and guarantees full path coverage when it terminates. We prove some basic properties of our technique and illustrate its practical usefulness through a prototype implementation.This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economia y Competitividad under grant TIN2013-44742-C4-1-R and by the Generalitat Valenciana under grant PROMETEOII/2015/013. Part of this research was done while the third author was visiting the University of Reunion; G. Vidal gratefully acknowledges their hospitality.Mesnard, F.; Payet, E.; Vidal Oriola, GF. (2015). Concolic Testing in Logic programming. Theory and Practice of Logic Programming. 15(4):711-725. https://doi.org/10.1017/S1471068415000332711725154SCHIMPF, J., & SHEN, K. (2011). ECLiPSe – From LP to CLP. Theory and Practice of Logic Programming, 12(1-2), 127-156. doi:10.1017/s1471068411000469Martelli, A., & Montanari, U. (1982). An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, 4(2), 258-282. doi:10.1145/357162.357169Godefroid, P., Klarlund, N., & Sen, K. (2005). DART. Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation - PLDI ’05. doi:10.1145/1065010.1065036Mera E. , López-García P. , and Hermenegildo M. V. 2009. Integrating software testing and run-time checking in an assertion verification framework. In 25th International Conference on Logic Programming, ICLP 2009, Pasadena. 281–295.Godefroid, P., Levin, M. Y., & Molnar, D. (2012). SAGE. Communications of the ACM, 55(3), 40. doi:10.1145/2093548.2093564WIELEMAKER, J., SCHRIJVERS, T., TRISKA, M., & LAGER, T. (2011). SWI-Prolog. Theory and Practice of Logic Programming, 12(1-2), 67-96. doi:10.1017/s1471068411000494CARLSSON, M., & MILDNER, P. (2011). SICStus Prolog—The first 25 years. Theory and Practice of Logic Programming, 12(1-2), 35-66. doi:10.1017/s1471068411000482Degrave F. , Schrijvers T. , and Vanhoof W. 2008. Automatic generation of test inputs for Mercury. In Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008. 71–86.Somogyi, Z., Henderson, F., & Conway, T. (1996). The execution algorithm of mercury, an efficient purely declarative logic programming language. The Journal of Logic Programming, 29(1-3), 17-64. doi:10.1016/s0743-1066(96)00068-4Vidal, G. (2015). Concolic Execution and Test Case Generation in Prolog. Lecture Notes in Computer Science, 167-181. doi:10.1007/978-3-319-17822-6_10Belli F. and Jack O. 1993. Implementation-based analysis and testing of Prolog programs. In ISSTA. 70–80.King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385-394. doi:10.1145/360248.360252Lloyd, J. W. (1987). Foundations of Logic Programming. doi:10.1007/978-3-642-83189-8Clarke L. 1976. A program testing system. In Proceedings of the 1976 Annual Conference (ACM'76). 488–491