  Verifiers that can prove programs correct against their full functional
specification require, for programs with loops, additional annotations in the
form of loop invariants---propeties that hold for every iteration of a loop. We
show that significant loop invariant candidates can be generated by
systematically mutating postconditions; then, dynamic checking (based on
automatically generated tests) weeds out invalid candidates, and static
checking selects provably valid ones. We present a framework that automatically
applies these techniques to support a program prover, paving the way for fully
automatic verification without manually written loop invariants: Applied to 28
methods (including 39 different loops) from various java.util classes
(occasionally modified to avoid using Java features not fully supported by the
static checker), our DYNAMATE prototype automatically discharged 97% of all
proof obligations, resulting in automatic complete correctness proofs of 25 out
of the 28 methods---outperforming several state-of-the-art tools for fully
automatic verification.
