Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking

Juan P. Galeotti, Carlo A. Furia, Eva May +2

Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants---prop…