Computing Exact Loop Bounds for Bounded Program Verification

Bounded program verification techniques verify functional properties of programs by analyzing the program for user-provided bounds on the number of objects and loop iterations. Whereas those two kinds of bounds are related, existing bounded program verification tools treat them as independent parameters and require the user to provide them. We present a new approach for automatically calculating exact loop bounds based on the number of objects; i.e. when a bound is found, it is always the precise one, thus ensuring that the verification is complete with respect to all the configurations of objects on the heap, enhancing the confidence in the correctness of the analyzed program. We compute the loop bounds by encoding the program and its specification as a logical formula and solve it using an SMT solver. We have performed experiments to evaluate the precision of our approach in loop bounds computation.