Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
A parametric segmentation functor for fully automatic and scalable array content analysis
Cousot P., Cousot R., Logozzo F. ACM SIGPLAN Notices46 (1):105-118,2011.Type:Article
Date Reviewed: Jun 1 2011

Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals for the static analysis of programs with arrays, the scalability of these analysis procedures has been an issue. This paper proposes a solution to this problem.

The central contribution of this paper is FunArray, a new abstract domain for arrays. FunArray is actually a functor that can take other abstract domains used for scalar variables and expressions and provide a domain for the arrays. This enables one to choose from the different analysis methods in the scalar variables and expressions, thereby making a tradeoff between precision and speed at the array level.

This abstraction is based on a novel and powerful symbolic representation of arrays as a sequence of consecutive nonoverlapping segments. The strength of this representation stems from the fact that it compactly represents the different cases that one needs to consider while abstracting a concrete array, making the analysis scalable.

The array abstraction is implemented in Clousot, a tool that can automatically generate invariants of programs involving array variables. Clousot has been used to successfully analyze several libraries in .NET that are beyond the reach of other existing techniques.

The authors of this paper are well-known experts in the field. The many examples, as well as the motivating beginning, definitely ease the readability of the paper. The paper is a bit cryptic, though, which is possibly due to size restrictions. An initial reading is likely to pose some difficulties for readers since the presentation contains some unexplained notations, such as “oo” for infinity. Some typographical errors in crucial places further complicate readability. Overall, though, the paper is accessible and useful for researchers working in the area of static analysis.

Reviewer:  S. Ramesh Review #: CR139100 (1112-1290)
Bookmark and Share
  Featured Reviewer  
 
Formal Methods (D.2.4 ... )
 
 
Mechanical Verification (F.3.1 ... )
 
 
Program Analysis (F.3.2 ... )
 
 
Semantics (D.3.1 ... )
 
 
Validation (D.2.4 ... )
 
 
Formal Definitions And Theory (D.3.1 )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy