Bounded program verification techniques verify functional properties of (data structure-rich) programs by analyzing given code with respect to a bounded domain in which the number of objects and loop iterations is bounded. Those two kinds of bounds are related. All existing bounded program verification tools, however, treat them as independent parameters and require the user to provide them. In this paper, we present a new approach for automatically calculating loop iteration bounds based on the number of objects, thus providing the user with an insight on what loop bounds to consider. Our approach computes both a lower and an upper bound for each loop by encoding the program and its pre-condition (if any exists) as a logical formula, and solving it for minimal and maximal loop iterations via iterative calls to an SMT solver. We can also determine whether the loop terminates or not for the bounded data. Various experiments are performed to demonstrate bound computations and non-termination detection.
Computing Loop Bounds for Bounded Program Verification, Tianhai Liu, Mana Taghdiri.
If you are interested in the BoundJ, please contact Tianhai Liu.