Date:
Thursday, October 28, 2010
Speaker:
Laura Kovacs
Venue: IST Austria
Notes:
Starts at 16:15
We describe Aligators, a tool for the generation of universally quantifiedarray invariants. Aligators leverages recurrence solving and algebraictechniques to carry out inductive reasoning over array content. The Aligatorsloop extraction module allows treatment of multi-path loops by exploiting theircommutativity and serializability properties. Our experience in applyingAligators on a collection of loops from open source software projects indicatesthe applicability of recurrence and algebraic solving techniques for reasoningabout arrays.
This is a joint work with T. Henzinger, T. Hottelier and A. Rybalchenko.
