Evènement pour le groupe Modélisation et Verification


Date 2010-05-27  11:30-12:45
TitreStatic 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.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurNicolas Halbwachs 
EmailNicolas.Halbwachs@imag.fr 
UrlVerimag, Grenoble 



Aucun document lié à cet événement.

Retour
Retour à l'index