Correspondence:
[†]
Address for correspondence: LIM - Université de la Réunion, 2 Rue Joseph Wetzell, Sainte-Clotilde 97490, Réunion, France
Note: [*] This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Ciencia, Innovación y Universidades/AEI under grant TIN2016-76843-C4-1-R and by the Generalitat Valenciana under grant Prometeo/2019/098 (DeepTrust).
Abstract: Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call “selective unification”. It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly.
