关于逻辑程序一致性测试中选择统一的完备性
On the Completeness of Selective Unification in Concolic Testing of Logic Programs
摘要：
Concolic测试是一种流行的动态验证技术，可用于模型检验和自动测试用例生成。我们最近在逻辑编程的上下文中引入了concolic测试。与以前的方法相比，这种设置的关键要素是一种技术，通过考虑原子可以与某些程序子句的头部统一的所有可能方式来生成适当的运行时目标。这就是所谓的“选择性”统一。在本文中，我们表明，现有的算法是不完整的，并探讨不同的替代品，以便有一个健全的和完整的算法选择性统一。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
