Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Simplifying Loop Invariant Generation Using Splitter Predicates
verfasst von : Rahul Sharma, Isil Dillig, Thomas Dillig, Alex Aiken
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.