LoopInvGen: A Loop Invariant Generator based on Precondition Inference
This addresses the challenge of automated program verification for developers, offering a more efficient and expressive tool compared to existing methods, though it builds incrementally on prior work.
The paper tackles the problem of automatically generating loop invariants to prove program correctness, presenting LoopInvGen, which starts with no initial features and synthesizes predicates on demand, achieving significantly faster performance on the SyGuS-COMP 2018 benchmarks.
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 (https://doi.org/10.1145/2908080.2908099). 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 2018 benchmarks from the INV track.