  Loop invariants play a central role in the verification of imperative
programs. However, finding these invariants is often a difficult and
time-consuming task for the programmer. We have previously shown how program
transformation can be used to facilitate the verification of functional
programs, but the verification of imperative programs is more challenging due
to the need to discover these loop invariants. In this paper, we describe a
technique for automatically discovering loop invariants. Our approach is
similar to the induction-iteration method, but avoids the potentially
exponential blow-up in clauses that can result when using this and other
methods. Our approach makes use of the distil- lation program transformation
algorithm to transform clauses into a simplified form that facilitates the
identification of similarities and differences between them and thus help
discover invariants. We prove that our technique terminates, and demonstrate
its successful application to example programs that have proven to be
problematic using other approaches. We also characterise the situations where
our technique fails to find an invariant, and show how this can be ameliorated
to a certain extent.
