|
Evènement pour le groupe Modélisation et Verification
Date | 2010-05-27 11:30-12:45 |
Titre | Static analysis of positional and non positional properties of arrays |
Résumé | (joint work with Mathias Péron and Valentin Perrelle)
Although array bound checking was a motivation of the very first
work on abstract interpretation, there are only few proposals about
dealing with array *contents* in program analysis. The reason is,
of course, that the general problem is difficult: array indexing
induces complex semantics, and in particular the possibility of
aliasing; moreover, since the size of an array can be large or
unknown, it represents a large or unbounded number of variables.
In this talk, we present two complementary analyses dealing with
properties of array contents in some simple cases: one-dimensional
arrays, traversed by simple "for" loops. Both analyses are based
on abstract interpretation:
- the first one aims at discovering positional properties of arrays
elements. For instance, it is able to discover that the result of
an insertion sort is a sorted array.
- the second one addresses non positional properties, like the
fact that, at some point of a program, the content of an array is
a permutation of its initial content.
|
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Nicolas Halbwachs |
Email | Nicolas.Halbwachs@imag.fr |
Url | Verimag, Grenoble |
Aucun document lié à cet événement. RetourRetour à l'index
| |