Abstract highlight: “Loop invariants play a major role in automatic verification of programs. Finding a suiting loop invariant can however be rather difficult. This thesis presents an implementation of automatic loop invariant inference based on postcondition mutation integrated directly within EVE.”
The invariants are usually developed in isolation with newcomers having more difficulty on that than pre- or post-conditions as described here. This is first work I saw that generates invariants from post-conditions. That might make it easier or just save time. Btw, EVE is Eiffel’s verification system.