ATCase

ATCase: an automatic generation tool of test case for numerical program based on polynomial constraint solving. The existing symbolic execution approach of automatic test case generation is defective because of the precision restrict and complexity for solving nonlinear 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 nonlinear 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 computation 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 nonlinear constraints.