Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Static analysis of programs manipulating arrays
du groupe Modélisation et Verification

Date 2014-02-20  11:00-12:00
TitreStatic analysis of programs manipulating arrays 
RésuméStatic analysis is a key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs, ...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections) Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition. The choice of this partition is a difficult problem and each method has its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes. We generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.  
Lieu076 
OrateurValentin Perrelle 
Emailvalentin.perrelle@irt-systemx.fr 
UrlIRT SystemX 



Aucun document lié à cet événement.

Retour
Retour à l'index