View Related Documents

Abstract

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

Fulltext Preview

Image of the first page of the fulltext document