Generating Loop Invariants for Program Verification by Transformation

TL;DR

This paper presents an automated technique using program transformation to discover loop invariants in imperative programs, improving verification efficiency and overcoming limitations of previous methods.

Contribution

It introduces a novel invariant discovery method based on clause transformation that avoids exponential complexity and demonstrates practical effectiveness.

Findings

Successfully applied to challenging example programs

Proven to terminate and identify invariants in many cases

Characterized scenarios where the method may fail

Abstract

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.