P. Cousot & R. Cousot, Array content static analysis by segmentation

Patrick Cousot and Radhia Cousot.
Array content static analysis by segmentation
Seminar, IBM T.J. Watson Research Center at Hawthorn, NY, April 24, 2010
Abstract:
     We present a parametric segmentation abstract functor for fully automatic and scalable inference of array content properties. The main idea is to automatically divide arrays into consecutive non-overlapping possibly empty segments whose content is abstracted uniformly. The array segmentation is automatically and semantically inferred during the static analysis depending on the way array elements are modified and accessed. The segment bounds are represented by symbolic expressions. The analysis of the segment element properties or the relation between the index and array value in segments is a parameter of the functor so as to tune the cost/ratio of the analysis.
     A prototype analyzer has been implemented to adjust the algorithms and obtain the appropriate precision/cost ratio before implementing the analysis in a professional static analyzer for object-oriented languages used in an industrial context. This has shown the analysis to scale up with satisfactory precision and cost contrary to previous attempts which did not scale properly or required more user interaction than can be sustained in a typical engineering project.
     Joint work with Francesco Logozzo, MSR.
Slides of the 60 mn presentation (to be used with Acrobat Reader):
- .pdf, 1 slide per page (2.7 Mb)
- .pdf, 4 slide per page (2.7 Mb)

Bibliographic reference:

\bibitem{CousotCousot-IBM-2010-04-24}
P.~Cousot and R.~Cousot.
\newblock Array content static analysis by segmentation.
\newblock Seminar, IBM T.J. Watson Research Center at Hawthorn, NY, April 24, 2010.

@inProceedings{CousotCousot-IBM-2010-04-24,
   author =    {P.~Cousot and R.~Cousot},
   title =     {Array content static analysis by segmentation},
   booktitle = {Seminar, IBM T.J. Watson Research Center},
   address =   {Hawthorn, NY, USA},
   month =     {24 April},
   year =      {2010},
}

Copyright notice
Last modified: Monday, 07-May-2012 17:51:03 EDT