Bachelor Thesis


Loop invariant inference from postconditions in EVE
Bachelor Thesis, November 2012 — June 2013
Author: Michael Ameri
Supervisors: Carlo A. Furia and Julian Tschannen
Project plan
Project report


Loop invariants are an indispensable ingredient of the correctness proofs of programs. At the same time, annotating a loop with suitable invariants is often a non-trivial task that resists complete automation. The availability of postconditions can help in this regard, as loop invariants are often expressible as mutations of the loop’s postcondition. The goal of this project is implementing a loop invariant inference technique based on postcondition mutation.