Computing Exact Loop Bounds for Bounded Program Verification

Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert, Mana Taghdiri


Bounded program verication 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 verication tools treat them as independent
parameters and require the user to provide them. We present a new approach for
automatically calculating exact loop bounds, i.e., the greatest lower bound
and the least upper bound, based on the number of objects. This ensures that
the verication is complete with respect to all the congurations of objects
on the heap and thus enhances the condence in the correctness of the
analyzed program. We compute the loop bounds by encoding the program and its
specication as a logical formula, and solve it using an SMT solver. We
performed experiments to evaluate the precision of our approach in loop bounds
computation.