Abstract
Abstract interpretation is a formal method that enables the static and automatic determination of run-time properties of programs. This method uses a characterization of program invariants as least and greatest fixed points of continuous functions over complete lattices of program properties. In this paper, we study precise and efficient chaotic iteration strategies for computing such fixed points when lattices are of infinite height and speedup techniques, known as widening and narrowing, have to be used. These strategies are based on a weak topological ordering of the dependency graph of the system of semantic equations associated with the program and minimize the loss in precision due to the use of widening operators. We discuss complexity and implementation issues and give precise upper bounds on the complexity of the intraprocedural and interprocedural abstract interpretation of higher-order programs based on the structure of their control flow graph.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Alfred V. Aho, Ravi Sethi and Jeffrey D. Ullman: “Compilers — Principles, Techniques and Tools”, Addison-Wesley Publishing Company (1986)
François Bourdoncle: “Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity”, Proc. of the International Workshop PLILP'90, Lecture Notes in Computer Science 456, Springer-Verlag (1990)
François Bourdoncle: “Abstract Interpretation By Dynamic Partitioning”, Journal of Functional Programming, Vol. 2, No. 4 (1992)
François Bourdoncle: “Sémantiques des langages impératifs d'ordre supérieur et interprétation abstraite”, Ph.D. dissertation, Ecole Polytechnique (1992)
François Bourdoncle: “Abstract Debugging of Higher-Order Imperative Languages”, Proc. of SIGPLAN '93 Conference on Programming Language Design and Implementation (1993)
Michael Burke: “An Interval-Based Approach to Exhaustive and Incremental Interprocedural Data-Flow Analysis”, ACM Transactions on Programming Languages and Systems, Vol. 12, Num. 3 (1990) 341–395
Patrick and Radhia Cousot: “Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints”, Proc. of the 4th ACM Symp. on POPL (1977) 238–252
Patrick Cousot: “Asynchronous iterative methods for solving a fixpoint system of monotone equations”, Research Report IMAG-RR-88, Université Scientifique et Médicale de Grenoble (1977)
Patrick Cousot and Nicolas Halbwachs: “Automatic discovery of linear constraints among variables of a program”, Proc. of the 5th ACM Symp. on POPL (1978) 84–97
Patrick Cousot: “Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis. Analyse sémantique de programmes”, Ph.D. dissertation, Université Scientifique et Médicale de Grenoble (1978)
Patrick Cousot: “Semantic foundations of program analysis”, in Muchnick and Jones Eds., Program Flow Analysis, Theory and Applications, Prentice-Hall (1981) 303–343
Alain Deutsch: “On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications”, Proc. of the 17th ACM Symp. on POPL (1990)
Alain Deutsch: “A Storeless Model of Aliasing and its Abstractions using Finite Representations of Right-Regular Equivalence Relations”, Proc. of the IEEE' 92 International Conference on Computer Languages, IEEE Press (1992)
Michael. R. Garey and David S. Johnson: “Computers and Intractability: A Guide to the Theory of NP-completeness”, W.H. Freeman and Company (1979)
Philippe Granger: “Static analysis of arithmetical congruences”, International Journal of Computer Mathematics (1989) 165–190
Larry G. Jones: “Efficient Evaluation of Circular Attribute Grammars”, ACM Transactions on Programming Languages and Systems, Vol. 12, Num. 3 (1990) 429–462
B. Le Charlier, K. Musumbu and P. Van Hentenryck: “A generic abstract interpretation algorithm and its complexity analysis”, in K. Furukawa editors, Proc. of the Eight International Conference on Logic Programming, MIT Press (1991) 64–78
B. Le Charlier and P. Van Hentenryck: “A universal top-down fixpoint algorithm”, Technical Report 92-1, Institute of Computer Science, University of Namur, Belgium (1992)
R.A. O'Keefe: “Finite fixed-point problems”, in J.-L. Lassez editor, Proc. of the Fourth International Conference of Logic Programming, MIT Press (1987) 729–743
R.E. Tarjan: “Depth-first search and linear graph algorithms”, SIAM J. Comput., 1 (1972) 146–160
R.E. Tarjan: “An Improved Algorithm for Hierarchical Clustering Using Strong Components”, Information Processing Letters 17, Elsevier Science Publishers B.V. (1983) 37–41
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bourdoncle, F. (1993). Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds) Formal Methods in Programming and Their Applications. Lecture Notes in Computer Science, vol 735. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039704
Download citation
DOI: https://doi.org/10.1007/BFb0039704
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57316-6
Online ISBN: 978-3-540-48056-3
eBook Packages: Springer Book Archive