You can manage bookmarks using lists, please log in to your user account for this.
Media type:
E-Article
Title:
Discovering properties about arrays in simple programs
Contributor:
Halbwachs, Nicolas;
Péron, Mathias
Published:
Association for Computing Machinery (ACM), 2008
Published in:
ACM SIGPLAN Notices, 43 (2008) 6, Seite 339-348
Language:
English
DOI:
10.1145/1379022.1375623
ISSN:
0362-1340;
1558-1160
Origination:
Footnote:
Description:
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 A I ; the new idea is to consider relational abstract properties ψ( A I , B I , ...) 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.