中文摘要：

现有的基于符号执行的测试用例自动生成技术存在不足之处：由于精度限制和非线性约束求解的复杂性，符号执行在遇到复杂的非线性浮点约束时效果并不理想．针对这一现状，给出了一个基于多项式约束求解和区间验证的测试用例生成算法．对于复杂非线性约束难以求解的问题，采用基于低秩矩量矩阵恢复的多项式系统求解方法，该方法对于含有等式和不等式的多项式系统，相较于其他方法求解速度更快，更适合大规模问题的求解；对于浮点约束求解不准确的问题，采用基于区间分析的验证算法来计算包含精确实解的区间，基于该区间给出测试用例，可以避免浮点计算的不准确和异常．结合该算法和符号执行工具KLEE—FP实现了一个测试用例自动生成工具ATCase（automatically genera tetest case），它能够分析数值程序中的路径并自动生成满足路径约束的测试用例．在两个开源软件库中的2两个复杂的真实程序上运行的实验结果表明ATCase相比KLEE—FP所使用的STP求解器，能快速生成具有更高覆盖率的测试用例，特别是在处理相对复杂的非线性约束时，优势更加明显．

英文摘要：

The existing symbolic execution approach of automatic test case gener- ation is defective because of the precision restrict and complexity for solving non- linear constrains, which make the result not satisfactory. For this deficiency, a test case generation algorithm based on polynomial system solving technique and interval verification is provided. Concretely, for the difficulty of solving non-linear constrains aspect, low-rank moment matrix recover based method to solve polynomial system is utilized, which is more efficient and suitable for big scale problems. For the inaccuracy results from computation, we make good use of interval arithmetic at the computa- tion procedure to provide an interval containing the real root of the system and then choose the test case from it as the result, which is more accurate avoiding false test cases from the computational error. In this paper, an automatic generation tool of test case for numerical program named ATCase is proposed. The theoretical bases of ATCase are the algorithm of computing real solutions of polynomial constraints, the interval analysis and the symbolic execution tool KLEE-FP. Experiments on 22 complicated real programs in open source projects show that the proposed tool is more effective and efficient than the STP solver of KLEE-FP, especially in case of complex non-linear constraints.