We present a framework for automating the discovery of loop invariants based upon failed proof attempts. The discovery of
suitable loop invariants represents a bottleneck for automatic verification of imperative programs. Using the proof planning
framework we reconstruct standard heuristics for developing invariants. We relate these heuristics to the analysis of failed
proof attempts allowing us to discover invariants through a process of refinement.
The contribution of the first author is supported by an EPSRC student ship award 96307451, and the contribution of the second
author is supported by EPSRC grant GR/L11724