Title: LoopInvGen: A Loop Invariant Generator based on Precondition Inference,
Abstract: We describe the LoopInvGen tool for generating loop invariants that can
provably guarantee correctness of a program with respect to a given
specification. LoopInvGen is an efficient implementation of the inference
technique originally proposed in our earlier work on PIE
(this https URL).
In contrast to existing techniques, LoopInvGen is not restricted to a fixed
set of features -- atomic predicates that are composed together to build
complex loop invariants. Instead, we start with no initial features, and use
program synthesis techniques to grow the set on demand. This not only enables a
less onerous and more expressive approach, but also appears to be significantly
faster than the existing tools over the SyGuS-COMP 2017 benchmarks from the INV
track.