On the completeness of selective unification in concolic testing of logic programs

DOI10.1007/978-3-319-63139-4_12MaRDI QIDQ2409737zbMATH OpenOpenAlexFDO

Authors Fred Mesnard, Étienne Payet, Germán Vidal

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.03054

Mathematics Subject Classification ID

Logic programming (68N17)

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.

Recommendations

• Selective Unification in (Constraint) Logic Programming*
• Concolic testing in logic programming
• Concolic testing in CLP
• Concolic execution and test case generation in Prolog
• Abstraction-driven concolic testing

Cited in

(9)

• An SMT-based concolic testing tool for logic programs
• Abstraction-driven concolic testing
• Concolic execution and test case generation in Prolog
• Concolic testing in logic programming
• Verification of the Completeness of Unification Algorithms à la Robinson
• Selective Unification in (Constraint) Logic Programming*
• Concolic testing in CLP
• Fundamental Approaches to Software Engineering
• Concolic execution in functional programming by program instrumentation

This page was built for publication: On the completeness of selective unification in concolic testing of logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409737)