Sciweavers

Share
CAV
2011
Springer

Simplifying Loop Invariant Generation Using Splitter Predicates

10 years 5 months ago
Simplifying Loop Invariant Generation Using Splitter Predicates
Abstract. We present a novel static analysis technique that substantially improves the quality of invariants inferred by standard loop invariant generation techniques. Our technique decomposes multi-phase loops, which require disjunctive invariants, into a semantically equivalent sequence of single-phase loops, each of which requires simple, conjunctive invariants. We define splitter predicates which are used to identify phase transitions in loops, and we present an algorithm to find useful splitter predicates that enable the phase-reducing transformation. We show experimentally on a set of representative benchmarks from the literature and real code examples that our technique substantially increases the quality of invariants inferred by standard invariant generation techniques. Our technique is conceptually simple, easy to implement, and can be integrated into any automatic loop invariant generator.
Rahul Sharma 0001, Isil Dillig, Thomas Dillig, Ale
Added 25 Aug 2011
Updated 25 Aug 2011
Type Journal
Year 2011
Where CAV
Authors Rahul Sharma 0001, Isil Dillig, Thomas Dillig, Alex Aiken
Comments (0)
books