Selective Unification in (Constraint) Logic Programming^*

Issue title: Special Issue on the 26th International Symposium on Logic-Based Program Synthesis and Transformation: LOPSTR 2016

Guest editors: Manuel Hermenegildo, Pedro López-García, Alberto Pettorossi and Maurizio Proietti

Article type: Research Article

Authors: Mesnard, Fred^{a; †} | Payet, Étienne^a | Vidal, Germán^b

Affiliations: [a] LIM - Université de la Réunion, Réunion, France. [email protected], [email protected] | [b] MiST, VRAIN, Universitat Politècnica de València, València, Spain. [email protected]

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.

Keywords: Logic programming, Constraint logic programming, Concolic testing, Unification

DOI: 10.3233/FI-2020-1993

Journal: Fundamenta Informaticae, vol. 177, no. 3-4, pp. 359-383, 2020