Improving the static analysis of loops by dynamic partitioning techniques

Many static analyses aim at assigning to each control point of a program an invariant property that characterizes any state of a trace corresponding to this point. The choice of the set of control points determines the states of an execution trace for which a common property must be found. We focus on sufficient conditions to substitute one control flow graph for another during an analysis. Next, we introduce a dynamic partitioning algorithm that improves the precision of the calculated invariants by deciding dynamically how to map the states of the traces to the control points, depending on the properties resulting from the first steps of the analysis. In particular, this algorithm enables the loops to be unfolded only if this improves the precision of the final invariants. Its correctness stems from the fact that it uses legal graph substitutions.