# A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

2 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Abstract : We introduce FunArray, a parametric segmentation abstract domain functor for the fully automatic and scalable analysis of array content properties. The functor enables a natural, painless and efficient lifting of existing abstract domains for scalar variables to the analysis of uniform compound data-structures such as arrays and collections (as well as matrices when instantiating the functor on itself). The analysis automatically and semantically divides arrays into consecutive non-overlapping possibly empty segments. Segments are delimited by sets of bound expressions and abstracted uniformly. All bound expressions appearing in a set are equal in the concrete. FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The bound expressions, the segment abstractions and the reduction operator are the three parameters of the analysis. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray inArrayal to adjust and experiment with the abstractions and the algorithms to obtain the appropriate precision/ratio cost. Then we implemented it into Clousot, an abstract interpretation-based static contract checker for .NET. We empirically validated the precision and the performance of the analysis by running it on the main libraries of .NET and on its own code. We were able to infer thousands of invariants and verify the implementation with a modest overhead (circa 1%). To the best of our knowledge this is the first analysis of this kind applied to such a large code base, and proven to scale.
Keywords :
Type de document :
Communication dans un congrès
ACM Press. Proceedings of the 38$^}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. 2011

Littérature citée [34 références]

https://hal.inria.fr/inria-00543874
Contributeur : Patrick Cousot <>
Soumis le : lundi 6 décembre 2010 - 18:01:58
Dernière modification le : mardi 24 avril 2018 - 17:20:13
Document(s) archivé(s) le : samedi 3 décembre 2016 - 01:57:31

### Fichier

POPL090-Cousot-Cousot-Logozzo....
Fichiers produits par l'(les) auteur(s)

### Identifiants

• HAL Id : inria-00543874, version 1

### Citation

Patrick Cousot, Radhia Cousot, Francesco Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. ACM Press. Proceedings of the 38$^}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. 2011. 〈inria-00543874〉

### Métriques

Consultations de la notice

## 180

Téléchargements de fichiers