Selective Unification in (Constraint) Logic Programming * - Université de La Réunion Access content directly
Journal Articles Fundamenta Informaticae Year : 2020

Selective Unification in (Constraint) Logic Programming *


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.
Fichier principal
Vignette du fichier
20-MesnardPV.pdf (491.43 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04500674 , version 1 (12-03-2024)



  • HAL Id : hal-04500674 , version 1


Frédéric Mesnard, Etienne Payet, Germán Vidal. Selective Unification in (Constraint) Logic Programming *. Fundamenta Informaticae, 2020, 177 (3-4), pp.359-383. ⟨hal-04500674⟩
16 View
5 Download


Gmail Mastodon Facebook X LinkedIn More