Comparison between Performance of Constraint Solver for Prediction Model in Symbolic Execution

Nowadays, automated software testing is too popular, and symbolic execution takes too much attention for software testing automation. Constraint solvers are used to solve the constraint set produced during the Symbolic Execution process. Various popular constraint solvers (Z3, mathsat, CVC4, Yices, boolector) are available. On average, constraint solver takes 90–98% of the total time symbolic execution. Constraint solver might get stuck in solving complex problems hence, degrades the overall performance of the symbolic execution. In literature timeout threshold-based solutions are given but they are not so efficient. One solution to this problem is to have a time prediction model which can predict the time required for solving a constraint model and checks whether to continue the ongoing solving process or not in symbolic execution. In this paper, we present this model in which we have used the Mathsat Constraint Solver to collect the data by running the GNU Coreutils program and Busybox utilities. The performance comparison of the different solvers was done over three constraint datasets.