Aligators for Arrays

Date: Thursday, October 28, 2010
Speaker: Laura Kovacs
Venue: IST Austria

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.

Posted in RiSE Seminar