Inferring loop invariants using postconditions

One of the obstacles in automatic program proving is to obtain suit-able 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 “uncou-pling ” 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 implemen-tation (freely available for download and currently relying on Microsoft Research’s Boogie tool), and the results obtained.