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., p_0 + p_1j + P_2k ≥ 0, for parameters p_0, p_1, and P_2, 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.
展开▼
