Generating Loop Invariants for Program Verification by Transformation

G. W. Hamilton
(School of Computing, Dublin City University, Republic of Ireland)

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.

In Alexei Lisitsa, Andrei P. Nemytykh and Maurizio Proietti: Proceedings Fifth International Workshop on Verification and Program Transformation (VPT 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 253, pp. 36–53.
Published: 23rd August 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: