Simplifying Loop Invariants Generation Using Splitter Predicates

We present a novel static analysis technique that substan- tially improves the quality of invariants inferred by standard loop invari- ant generation techniques. Our technique decomposes multi-phase loops, which require disjunctive invariants, into a semantically equivalent se- quence of single-phase loops, each of which requires simple, conjunctive invariants. We dene splitter predicates which are used to identify phase transitions in loops, and we present an algorithm to nd useful split- ter predicates that enable the phase-reducing transformation. We show experimentally on a set of representative benchmarks from the litera- ture and real code examples that our technique substantially increases the quality of invariants inferred by standard invariant generation tech- niques. Our technique is conceptually simple, easy to implement, and can be integrated into any automatic loop invariant generator.