Recursive symbolic bound analysis in loop structure

This paper proposes a novel approach to symbolic bound analysis in loop structure. Our method is precise to analyze nonlinear correlated induction variables in the multi-loop and multi-branch programs by structure analysis with solutions of symbolic equations and inequalities. Based on the symbolic operation, the bounds of induction variables with analytical algebraic representations could be solved. This method performs effectively at the analysis of the symbolic (also numeric) bounds of array indices, pointers and other complicate variables in loop structures. Experimental results from our prototype implementation indicate that this technology could be used in practical detections to solve those bound problems.