Aligators for Arrays (Tool Paper)

8 years 3 months ago
Aligators for Arrays (Tool Paper)
This paper presents Aligators, a tool for the generation of universally quantified array invariants. Aligators leverages recurrence solving and algebraic techniques to carry out inductive reasoning over array content. The Aligators’ loop extraction module allows treatment of multi-path loops by exploiting their commutativity and serializability properties. Our experience in applying Aligators on a collection of loops from open source software projects indicates the applicability of recurrence and algebraic solving techniques for reasoning about arrays.
Thomas A. Henzinger, Thibaud Hottelier, Laura Kov&
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LPAR
Authors Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrey Rybalchenko
Comments (0)