LoopInvGen: A Loop Invariant Generator based on Precondition Inference

We present LoopInvGen, a tool for generating loop invariants that can provably guarantee correctness of a program with respect to a given specification. We extend the data-driven approach to inferring sufficient loop invariants from a collection of program states. In contrast to existing data-driven 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. Compared to existing static and dynamic techniques for loop invariant inference, not only does LoopInvGen enable a less onerous and more expressive approach, but is also significantly faster over the SyGuS-INV (2017) benchmarks.