Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-23T21:32:21.375Z Has data issue: false hasContentIssue false
  • English
  • Français

Concolic Testing in CLP

Published online by Cambridge University Press:  21 September 2020

FRED MESNARD ,
ÉTIENNE PAYET  and
GERMÁN VIDAL Open the ORCID record for GERMÁN VIDAL [Opens in a new window]
FRED MESNARD
Affiliation:
LIM - Université de la Réunion, France (e-mail: [email protected], [email protected])
ÉTIENNE PAYET
Affiliation:
LIM - Université de la Réunion, France (e-mail: [email protected], [email protected])
GERMÁN VIDAL
Affiliation:
MiST, VRAIN, Universitat Politècnica de València (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

CLPverificationconcolic testing
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 20 , Issue 5: 36th International Conference on Logic Programming Special Issue I , September 2020 , pp. 671 - 686
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

This author has been partially supported by EU (FEDER) and Spanish MCI/AEI under grants TIN2016-76843-C4-1-R and PID2019-104735RB-C41, and by the Generalitat Valenciana under grant Prometeo/2019/098 (DeepTrust).

References

Apt, K. R. 1997. From Logic Programming to Prolog. Prentice Hall.Google Scholar
Comon, H. and Kirchner, C. 1999. Constraint solving on terms. In Constraints in Computational Logics: Theory and Applications, International Summer School, CCL’99, Revised Lectures, Comon, H., Marché, C., and Treinen, R., Eds. Lecture Notes in Computer Science, vol. 2002. Springer, 47–103.Google Scholar
Fortz, S., Mesnard, F., Payet, É., 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.Google Scholar
Gallagher, J. P. and Bruynooghe, M. 1991. The derivation of an algorithm for program specialisation. New Generation Computing 9, 3/4, 305–334.Google Scholar
Gange, G., Navas, J. A., Schachte, P., Søndergaard, H., and Stuckey, P. J. 2015. Horn clauses as an intermediate representation for program analysis and transformation. Theory and Practice of Logic Programming 15, 4-5, 526–542.CrossRefGoogle Scholar
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–148.Google Scholar
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–223.Google Scholar
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–361.Google Scholar
Jaffar, J., Maher, M. J., Marriott, K., and Stuckey, P. J. 1998. The semantics of constraint logic programs. Journal of Logic Programming 37, 1-3, 1–46.Google Scholar
King, J. C. 1976. Symbolic execution and program testing. Commun. ACM 19, 7, 385–394.CrossRefGoogle Scholar
Leuschel, M. and Schreye, D. D. 1998. Constrained partial deduction and the preservation of characteristic trees. New Generation Computing 16, 3, 283–342.10.1007/BF03037483CrossRefGoogle Scholar
Lloyd, J. W. and Shepherdson, J. C. 1991. Partial evaluation in logic programming. J. Log. Program. 11, 3&4, 217–242.Google Scholar
Mesnard, F., Payet, É., and Vidal, G. 2015a. Concolic testing in logic programming. Theory and Practice of Logic Programming 15, 4-5, 711–725.CrossRefGoogle Scholar
Mesnard, F., Payet, É., and Vidal, G. 2015b. Contest website. URL: http://kaz.dsic.upv.es/contest.html.Google Scholar
Mesnard, F., Payet, É., 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’17), Vanhoof, W. and Pientka, B., Eds. ACM, 115–126.Google Scholar
Mesnard, F., Payet, É., and Vidal, G. 2020. Concolic Testing in CLP. CoRR abs/2008.00421.Google Scholar
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–292.Google Scholar
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’08), de la Banda, M. G. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer, 693–697.Google Scholar
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–423.Google Scholar
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–272.Google Scholar
Somogyi, Z., Henderson, F., and Conway, T. C. 1996. The execution algorithm of Mercury, an efficient purely declarative logic programming language. J. Log. Program. 29, 1-3, 17–64.CrossRefGoogle Scholar
Ströder, 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’11), G. Vidal, Ed. Notes, Lecture in Computer Science, vol. 7225. Springer, 237–252.Google Scholar
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–235.Google Scholar
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–181.Google Scholar