Paper Info
Title
Aligators For Arrays (Tool Paper)
Abstract
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.
Year
DOI
Venue
2010
10.1007/978-3-642-16242-8_25
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING
Keywords
Field
DocType
inductive reasoning
Inductive reasoning,Serializability,Programming language,Algebraic number,Commutative property,Computer science,Theoretical computer science,Invariant (mathematics),Loop counter,Open source software
Conference
Volume
ISSN
Citations 
6397
0302-9743
2
PageRank 
References 
Authors
0.42
12
4
Name
Order
Citations
PageRank
Thomas A. Henzinger1148271317.51
Thibaud Hottelier21419.16
Laura Kovács349436.97
Andrey Rybalchenko4143968.53