{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:54Z","timestamp":1747173654218,"version":"3.40.5"},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T00:00:00Z","timestamp":1600646400000},"content-version":"unspecified","delay-in-days":20,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2020,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Concolic testing is a popular software verification technique based on a combination of concrete and symbolic execution. Its main focus is finding bugs and generating test cases with the aim of maximizing code coverage. A previous approach to concolic testing in logic programming was not sound because it only dealt with positive constraints (by means of substitutions) but could not represent negative constraints. In this paper, we present a novel framework for concolic testing of CLP programs that generalizes the previous technique. In the CLP setting, one can represent both positive and negative constraints in a natural way, thus giving rise to a sound and (potentially) more efficient technique. Defining verification and testing techniques for CLP programs is increasingly relevant since this framework is becoming popular as an intermediate representation to analyze programs written in other programming paradigms.<\/jats:p>","DOI":"10.1017\/s1471068420000216","type":"journal-article","created":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T05:25:42Z","timestamp":1600665942000},"page":"671-686","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Concolic Testing in CLP"],"prefix":"10.1017","volume":"20","author":[{"given":"FRED","family":"MESNARD","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9TIENNE","family":"PAYET","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1857-6951","authenticated-orcid":false,"given":"GERM\u00c1N","family":"VIDAL","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,9,21]]},"reference":[{"key":"S1471068420000216_ref12","unstructured":"12. Lloyd, J. W. and Shepherdson, J. C. 1991. Partial evaluation in logic programming. J. Log. Program. 11, 3&4, 217\u2013242."},{"key":"S1471068420000216_ref4","unstructured":"4. Gallagher, J. P. and Bruynooghe, M. 1991. The derivation of an algorithm for program specialisation. New Generation Computing 9, 3\/4, 305\u2013334."},{"key":"S1471068420000216_ref19","unstructured":"19. Sen, K. and Agha, G. 2006. CUTE and jcute: Concolic unit testing and explicit path model-checking tools. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), Ball, T. and Jones, R. B. , Eds. Lecture Notes in Computer Science, vol. 4144. Springer, 419\u2013423."},{"key":"S1471068420000216_ref9","first-page":"1","article-title":"The semantics of constraint logic programs","volume":"1","author":"Jaffar","year":"1998","journal-title":"Journal of Logic Programming 37"},{"key":"S1471068420000216_ref20","unstructured":"20. Sen, K. , Marinov, D. , and Agha, G. 2005. CUTE: a concolic unit testing engine for C. In Proc. of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Wermelinger, M. and Gall, H. C. , Eds. ACM, 263\u2013272."},{"key":"S1471068420000216_ref24","unstructured":"24. Vidal, G. 2014. Concolic execution and test case generation in Prolog. In Proc. of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2014), Proietti, M. and Seki, H. , Eds. Lecture Notes in Computer Science, vol. 8981. Springer, 167\u2013181."},{"key":"S1471068420000216_ref17","unstructured":"17. Palacios, A. and Vidal, G. 2015. Concolic execution in functional programming by program instrumentation. In Proc. of the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), M. Falaschi, Ed. Notes, Lecture in Computer Science, vol. 9527. Springer, 277\u2013292."},{"key":"S1471068420000216_ref15","unstructured":"15. Mesnard, F. , Payet, \u00c9. , and Vidal, G. 2017. Selective unification in constraint logic programming. In Proc. of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP\u201917), Vanhoof, W. and Pientka, B. , Eds. ACM, 115\u2013126."},{"key":"S1471068420000216_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"S1471068420000216_ref14","unstructured":"14. Mesnard, F. , Payet, \u00c9. , and Vidal, G. 2015b. Contest website. URL: http:\/\/kaz.dsic.upv.es\/contest.html."},{"key":"S1471068420000216_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000332"},{"key":"S1471068420000216_ref18","unstructured":"18. Schrijvers, T. , Costa, V. S. , Wielemaker, J. , and Demoen, B. 2008. Towards typed Prolog. In Proc. of the 24th International Conference on Logic Programming (ICLP\u201908), de la Banda, M. G. and Pontelli, E. , Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 693\u2013697."},{"key":"S1471068420000216_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"S1471068420000216_ref3","unstructured":"3. Fortz, S. , Mesnard, F. , Payet, \u00c9. , Perrouin, G. , Vanhoof, W. , and Vidal, G. 2020. An SMT-based concolic testing tool for logic programs (poster). In Proc. of the 15th International Symposium on Functional and Logic Languages (FLOPS 2020), Nakano, K. and Sagonas, K. , Eds. Springer LNCS. To appear. Extended version at https:\/\/arxiv.org\/abs\/2002.07115."},{"key":"S1471068420000216_ref7","unstructured":"7. Godefroid, P. , Klarlund, N. , and Sen, K. 2005. DART: directed automated random testing. In Proc. of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005), Sarkar, V. and Hall, M. W. , Eds. ACM, 213\u2013223."},{"key":"S1471068420000216_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000204"},{"key":"S1471068420000216_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037483"},{"key":"S1471068420000216_ref23","unstructured":"23. Stulova, N. , Morales, J. F. , and Hermenegildo, M. V. 2014. Assertion-based debugging of higher-order (C)LP programs. In Proc. of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014), Chitil, O. , King, A. , and Danvy, O. , Eds. ACM, 225\u2013235."},{"key":"S1471068420000216_ref2","volume-title":"Computer Science","volume":"2002","author":"Comon","year":"1999"},{"key":"S1471068420000216_ref16","unstructured":"16. Mesnard, F. , Payet, \u00c9. , and Vidal, G. 2020. Concolic Testing in CLP. CoRR abs\/2008.00421."},{"volume-title":"From Logic Programming to Prolog","year":"1997","author":"Apt","key":"S1471068420000216_ref1"},{"key":"S1471068420000216_ref6","unstructured":"6. Giantsios, A. , Papaspyrou, N. S. , and Sagonas, K. 2015. Concolic testing for functional languages. In Proc. of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP 2015), Falaschi, M. and Albert, E. , Eds. ACM, 137\u2013148."},{"key":"S1471068420000216_ref22","unstructured":"22. Str\u00f6der, T. , Emmes, F. , Schneider-Kamp, P. , Giesl, J. , and Fuhs, C. 2011. A linear operational semantics for termination and complexity analysis of ISO Prolog. In Proc. of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR\u201911), G. Vidal, Ed. Notes, Lecture in Computer Science, vol. 7225. Springer, 237\u2013252."},{"key":"S1471068420000216_ref8","unstructured":"8. Gurfinkel, A. , Kahsai, T. , Komuravelli, A. , and Navas, J. A. 2015. The SeaHorn verification framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Kroening, D. and Pasareanu, C. S. , Eds. Lecture Notes in Computer Science, vol. 9206. Springer, 343\u2013361."}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068420000216","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T08:48:44Z","timestamp":1610614124000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068420000216\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["S1471068420000216"],"URL":"https:\/\/doi.org\/10.1017\/s1471068420000216","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2020,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}