Verification constraint problems with strengthening

Abstract

The deductive method reduces verification of safety properties of programs to, first, proposing inductive assertions and, second, proving the validity of the resulting set of first-order verification conditions. We discuss the transition from verification conditions to verification constraints that occurs when the deductive method is applied to parameterized assertions instead of fixed expressions (e.g., p0 + P1j + p2k ≥ 0, for parameters p0, P1, and p2, instead of 3 + j - k ≥ 0) in order to discover inductive assertions. We then introduce two new verification constraint forms that enable the incremental and property-directed construction of inductive assertions. We describe an iterative method for solving the resulting constraint problems. The main advantage of this approach is that it uses off-the-shelf constraint solvers and thus directly benefits from progress in constraint solving. © Springer-Verlag Berlin Heidelberg 2006.