Abstract
Concolic testing is a popular dynamic validation technique that can be used for both model checking and automatic test case generation. We have recently introduced concolic testing in the context of logic programming. In contrast to previous approaches, the key ingredient in this setting is a technique to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. This is called “selective” unification. In this paper, we show that the existing algorithm is not complete and explore different alternatives in order to have a sound and complete algorithm for selective unification.
This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economía y Competitividad under grants TIN2013-44742-C4-1-R and TIN2016-76843-C4-1-R, and by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Following the linear semantics of [12], we consider sequences of goals to represent the leaves of the SLD tree built so far.
References
Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstraction. STTT 11(1), 53–67 (2009)
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, Englewood Cliffs (1997)
Clarke, L.A.: A program testing system. In: Proceedings of the 1976 Annual Conference (ACM 1976), pp. 488–491 (1976)
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI 2005, pp. 213–223. ACM (2005)
Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. CACM 55(3), 40–44 (2012)
King, J.C.: Symbolic execution and program testing. CACM 19(7), 385–394 (1976)
Mesnard, F., Payet, É., Vidal, G.: Concolic testing in logic programming. TPLP 15(4–5), 711–725 (2015)
Mesnard, F., Payet, É., Vidal, G.: Concolic testing in logic programming (extended version). CoRR abs/1507.05454 (2015). http://arxiv.org/abs/1507.05454
Palamidessi, C.: Algebraic properties of idempotent substitutions. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 386–399. Springer, Heidelberg (1990). doi:10.1007/BFb0032046
Pasareanu, C.S., Rungta, N., PathFinder, S.: symbolic execution of Java bytecode. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE, pp. 179–180. ACM (2010)
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)
Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., Fuhs, C.: A linear operational semantics for termination and complexity analysis of ISO Prolog. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 237–252. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32211-2_16
Acknowledgements
We would like to thank the anonymous reviewers and the participants of LOPSTR 2016 for their suggestions to improve this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Mesnard, F., Payet, É., Vidal, G. (2017). On the Completeness of Selective Unification in Concolic Testing of Logic Programs. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-63139-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-63138-7
Online ISBN: 978-3-319-63139-4
eBook Packages: Computer ScienceComputer Science (R0)