An approach for automatically generating loop invariants usingquantifier-elimination is proposed. An invariant of a loop is hypothesized asa parameterized formula. Parameters in the invariant are discovered by generatingconstraints on the parameters by ensuring that the formula is indeedpreserved by the execution path corresponding to every basic cycle of the loop.The parameterized formula can be successively refined by considering executionpaths one by one; heuristics can be developed for determining the order inwhich the paths are considered. Initialization of program variables as well asthe precondition and postcondition of the loop, if available, can also be usedto further refine the hypothesized invariant. Constraints on parameters generatedin this way are solved for possible values of parameters. If no solution ispossible, this means that an invariant of the hypothesized form does not existfor the loop. Otherwise, if the parametric constraints are solvable, then undercertain conditions on methods for generating these constraints, the strongestpossible invariant of the hypothesized form can be generated from most generalsolutions of the parametric constraints. The approach is illustrated using thefirst-order theory of polynomial equations as well as Presburger arithmetic.
展开▼
