Inferring Loop Invariants using Postconditions

TL;DR

This paper introduces a method for automatically inferring loop invariants by leveraging postconditions, using heuristics to improve inference across diverse algorithms, implemented within the Boogie verification framework.

Contribution

It presents a novel approach that infers loop invariants from postconditions using heuristics, enhancing automation in program verification.

Findings

Successfully infers invariants for various algorithms

Implemented in the Boogie verification tool

Achieves effective invariant inference using heuristics

Abstract

One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained.