Data-Driven Loop Invariant Inference with Automatic Feature Synthesis

07/07/2017

∙

by   Saswat Padhi, et al.

∙

0

∙

share

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. We compare with existing static and dynamic tools for loop invariant inference, and show that LoopInvGen enables a less onerous and more expressive form of inference.