Abstract
Much of the earlier development of abstract interpretation, and its application to imperative programming languages, has concerned techniques for finding fixed points in large (often infinite) lattices. The standard approach in the abstract interpretation of functional languages has been to work with small, finite lattices and this supposedly circumvents the need for such techniques. However, practical experience has shown that, in the presence of higher order functions, the lattices soon become too large (although still finite) for the fixed-point finding problem to be tractable. This paper develops some approximation techniques which were first proposed by Hunt and shows how these techniques relate to the earlier use of widening and narrowing operations by the Cousots.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
G. L. Burn, C. L. Hankin and S. Abramsky, Strictness Analysis for Higherorder functions, Science of Computer Programming 7 (1986), pp 249–278, North-Holland.
P. Cousot, Méthodes Itératives de Construction et d'Approximation de Points Fixes d'Opérateurs Monotones sur un Treilli, Analyse Sémantique des Programmes, Thèse d'Etat, Université de Grenoble, 1978.
P. Cousot, Semantic foundations of program analysis, in Muchnick S. S. and Jones N. D. (eds) Program Flow Analysis, pp 303–342, Prentice-Hall, 1981.
C. Clack and S. L. Peyton Jones, Strictness Analysis — a practical approach, in J.-P. Jouannaud (ed), Functional Programming Languages and Computer Architecture, LNCS 201, pp 352–49, Springer Verlag.
G. K. Gierz, K. H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, A Compendium of Continuous Lattices, Springer Verlag.
S. Hunt, Frontiers and open sets in abstract interpretation, in D. MacQueen (ed), Functional Programming Languages and Computer Architecture, pp 1–11, ACM Press.
S. Hunt and C. L. Hankin, Fixed Points and Frontiers: a new perspective, Journal of Functional Programming 1(1), pp 91–120, Cambridge University Press.
Jones N. D. and Mycroft A. Dataflow Analysis of Applicative Programs using Minimal Function Graphs, privately circulated manuscript, October 1985.
A. R. Meyer, Complexity of Program Flow Analysis for Strictness: Application of a Fundamental Theorem of Denotational Semantics, private communication.
C. C. Martin and C. L. Hankin, Finding Fixed Points in Finite Lattices, in G. Kahn (ed), Functional Programming Languages and Computer Architecture, LNCS 274, pp 426–445, Springer Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hankin, C., Hunt, S. (1992). Approximate fixed points in abstract interpretation. In: Krieg-Brückner, B. (eds) ESOP '92. ESOP 1992. Lecture Notes in Computer Science, vol 582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55253-7_13
Download citation
DOI: https://doi.org/10.1007/3-540-55253-7_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55253-6
Online ISBN: 978-3-540-46803-5
eBook Packages: Springer Book Archive