Paper Info
Title
Discovering properties about arrays in simple programs
Abstract
Array bound checking and array dependency analysis (for parallelization) have been widely studied. However, there are much less results about analyzing properties of array contents. In this paper, we propose a way of using abstract interpretation for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple "for" loops. The basic idea, borrowed from [GRS05], consists in partitioning arrays into symbolic intervals (e.g., [1,i -- 1], [i,i], [i + 1,n]), and in associating with each such interval I and each array A an abstract variable AI; the new idea is to consider relational abstract properties ψ(AI, BI, ...) about these abstract variables, and to interpret such a property pointwise on the interval I: ∀l ∈ I, ψ(A[l], B[l],...). The abstract semantics of our simple programs according to these abstract properties has been defined and implemented in a prototype tool. The method is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a "sentinel", the index stays within the bounds.
Year
DOI
Venue
2008
10.1145/1379022.1375623
Sigplan Notices
Keywords
Field
DocType
program verification,abstract interpretation,invariant synthesis,arrays,sorting algorithms,"sentinel"
Programming language,Tree traversal,Abstract interpretation,Computer science,Insertion sort,Static analysis,Sorted array,Theoretical computer science,Invariant (mathematics),Sorting algorithm,Pointwise
Conference
Volume
Issue
ISSN
43
6
0362-1340
Citations 
PageRank 
References 
72
2.30
13
Authors
2
Name
Order
Citations
PageRank
Nicolas Halbwachs13957426.43
Mathias Péron2853.11