Loading...
Please wait, while we are loading the content...
Similar Documents
Discovering properties about arrays in simple programs
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Halbwachs, Nicolas Péron, Mathias |
| Copyright Year | 2008 |
| 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. |
| Related Links | https://hal.science/hal-00288274/file/pldi.pdf |
| Conference Proceedings | PLDI 2008 |
| Language | English |
| Publisher | HAL CCSD |
| Publisher Date | 2008-06-01 |
| Access Restriction | Open |
| Subject Keyword | abstract interpretation sorting algorithms invariant synthesis Program verification |
| Content Type | Text |
| Resource Type | Conference Proceedings |
| Subject | Computer Science |
