Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Precise widening operators for convex polyhedra
Bagnara R., Hill P., Ricci E., Zaffanella E. Science of Computer Programming58 (1-2):28-56,2005.Type:Article
Date Reviewed: May 5 2006

Automated analysis that uses abstract interpretation techniques for complex systems, like software and hybrid-system models, involves computing fixpoints of the sequence of approximate behavior structures of the systems. In general, the sequence is infinite and slowly converges to the fixpoint. To speed up the convergence and to obtain an approximation of the limit point, the technique of widening is used. Widening attempts to convert an infinite sequence of approximations to a finite sequence so that the fixpoint of the original sequence can be computed. Typically, widening is carried out using a binary operator that takes a pair of approximations and produces an upper bound of the pair; this ensures faster convergence of the sequence. Many widening operators have been defined in the literature, starting with the standard operator, defined over convex polyhedra by Halbwachs and Cousot. Most analysis and verification tools that employ convex polyhedra use this operator. Other techniques like extrapolation (a weaker form of widening) and delaying the application of widening on a sequence have also been employed with limited success.

This paper provides a general framework to obtain new widening operators over arbitrary domains. The framework also provides a number of heuristics for obtaining new operators from old ones, and at the same time improving them. This framework has been instantiated in the domain of convex polyhedra, and several new operators and many existing operators proposed in the literature are derived in a systematic way. The framework makes use of a revised definition of widening, which is implemented in the Parma Polyhedral Library, and experiments with several interesting examples and heuristics demonstrate preliminary success.

The paper contains much useful material on widening and convex polyhedra that will be of use to both novice and experienced researchers. The paper is a bit difficult to read, with many cross-references to other works on the subject. It is advisable to read a few of the cited papers [1,2,3] before reading this paper.

Reviewer:  S. Ramesh Review #: CR132745 (0702-0170)
1) Besson, F.; Jensen, T.P.; Talpin, J.-P. Static analysis: Proceedings of the 6th International Symposium (LNCS 1694). Springer-Verlag, , 1999.
2) Cousot, P.; Halbwachs, N. Automatic discovery of linear restraints among variables of a program. In Conference record of the Fifth Annual ACM Symposium on Principles of Programming Languages ACM, 1978, 84–96.
3) Halbwachs, N. Détermination automatique de relations linéaires vérifiées par les variables d’un programme, Thèse de 3ème cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France, March 1979.
Bookmark and Share
  Featured Reviewer  
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
 
Formal Methods (D.2.4 ... )
 
 
Program Analysis (F.3.2 ... )
 
 
Relation Systems (I.2.4 ... )
 
 
Semantics Of Programming Languages (F.3.2 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Specifying And Verifying And Reasoning About Programs": Date
Programming: the derivation of algorithms
Kaldewaij A., Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780132041089)
Aug 1 1991
An introduction to programming with specifications
Kubiak R., Rudziński R., Sokolowski S., Academic Press Prof., Inc., San Diego, CA, 1991. Type: Book (9780124276208)
Jun 1 1992
Observational implementation of algebraic specifications
Hennicker R. Acta Informatica 28(3): 187-230, 1991. Type: Article
Jul 1 1992
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