Invariant Discovery via Failed Proof Attempts

We present a framework for automating the discovery of loop invariants based upon failed proof attempts. The discovery of suitable loop invariants is a bottle neck 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 an invariant through a process of refinement