Comparing the Galois connection and widening/narrowing approaches to abstract interpretation

  • Patrick Cousot
  • Radhia Cousot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 631)

Abstract

The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices (or lattices satisfying the chain condition).

Keywords

Logic Program Chain Condition Abstract Interpretation Type Node Type Graph 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AH87]
    S. Abramsky and G. Hankin, editors. Abstract Interpretation of Declarative Languages. Computers and their Applications. Ellis Horwood, Chichester, U.K., 1987.Google Scholar
  2. [BJCD87]
    M. Bruynooghe, G. Janssens, A. Gallebaut, and B. Demoen. Abstract interpretation: towards the global optimization of Prolog programs. In Proceedings of the 1987 International Symposium on Logic Programming, San Francisco, California, pages 192–204. IEEE Computer Society Press, Los Alamitos, California, August 31–September 4, 1987.Google Scholar
  3. [BK89]
    V. Balasundaram and K. Kennedy. A technique for summarizing data access and its use in parallelism enhancing transformations. In SIGPLAN'89 Conference on Programming Language Design and Implementation, pages 41–53, Portland, Oregon, June 21–23, 1989.Google Scholar
  4. [Bou90]
    F. Bourdoncle. Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In P. Deransart and Maluszyński, editors, Proceedings of the International Workshop PLILP'90, Programming Language Implementation and Logic Programming, Linköping, Sweden, Lecture Notes in Computer Science 456, pages 307–323. Springer-Verlag, Berlin, Germany, August 20–22, 1990.Google Scholar
  5. [Bou92]
    F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 1992. (to appear).Google Scholar
  6. [CC76]
    P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.Google Scholar
  7. [CC77a]
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977.Google Scholar
  8. [CC77b]
    P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E.J. Neuhold, editor, IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., Canada, pages 237–277. North-Holland Pub. Co., Amsterdam, the Netherlands, 1977.Google Scholar
  9. [CC79a]
    P. Cousot and R. Cousot. Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics, 82(1):43–57, 1979.Google Scholar
  10. [CC79b]
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages, pages 269–282, San Antonio, Texas, 1979.Google Scholar
  11. [CC92a]
    P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2–3), 1992. (to appear).Google Scholar
  12. [CC92b]
    P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 1992. (to appear).Google Scholar
  13. [CC92c]
    P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM Symposium on Principles of Programming Languages, pages 83–94, Albuquerque, New Mexico, 1992.Google Scholar
  14. [CH78]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the 5th ACM Symposium on Principles of Programming Languages, pages 84–97, Tucson, Arizona, 1978.Google Scholar
  15. [Cou78]
    P. 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. Thèse d'état ès sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, France, 21 March 1978.Google Scholar
  16. [Cou81]
    P. Cousot. Semantic foundations of program analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.Google Scholar
  17. [Deu92]
    A. Deutsch. A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations. In Proceedings of the 1992 International Conference on Computer Languages, Oakland, California, pages 2–13. IEEE Computer Society Press, Los Alamitos, California, April 20–23, 1992.Google Scholar
  18. [Gra89]
    P. Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30:165–190, 1989.Google Scholar
  19. [Gra91a]
    P. Granger. Analyses sémantiques de congruence. Thèse de l'école Polytechnique en informatique, LIX, école Polytechnique, Palaiseau, France, 12 July 1991.Google Scholar
  20. [Gra91b]
    P. Granger. Static analysis of linear congruence equalities among variables of a program. In S. Abramsky and T.S.E. Maibaum, editors, TAPSOFT'91, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, U.K., Volume 1 (CAAP'91), Lecture Notes in Computer Science 493, pages 169–192. Springer-Verlag, Berlin, Germany, 1991.Google Scholar
  21. [Hal79]
    N. Halbwachs. 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, 12 March 1979.Google Scholar
  22. [HH90]
    C. Hankin and S. Hunt. Approximate fixed points in abstract interpretation. In B. Krieg-Brückner, editor, Proceedings of the 4 th European Symposium on Programming, ESOP '92, pages 219–232. Springer-Verlag, Berlin, Germany, Rennes, France, February 26–28 1990.Google Scholar
  23. [JB92]
    G. Janssens and M. Bruynooghe. On abstracting the procedural behaviour of logic programs. In A. Voronkov, editor, Proceedings of the First Russian Conference on Logic Programming, Irkutsk, Russia, September 14–18, 1990 and of the Second Russian Conference on Logic Programming, St. Petersburg, Russia, September 11–16, 1991, pages 240–262. Springer-Verlag, Berlin, Germany, 1992.Google Scholar
  24. [KN87]
    R. B. Kieburtz and M. Napierala. Abstract semantics. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, chapter 7, pages 143–180. Ellis Horwood, Chichester, U.K., 1987.Google Scholar
  25. [MS88]
    K. Marriott and H. SØndergaard. On describing success patterns of logic programs. Technical Report 88/12, Department of Computer Science, University of Melbourne, Melbourne, Australia, 1988.Google Scholar
  26. [Myc80]
    A. Mycroft. The theory and practice of transforming call-by-need into call-by-value. In B. Robinet, editor, Proceedings of the Fourth International Symposium on Programming, Paris, France, 22–24 April 1980 Lecture Notes in Computer Science 83, pages 270–281. Springer-Verlag, Berlin, Germany, 1980.Google Scholar
  27. [Str88]
    J. Stransky. Analyse sémantique de structures de données dynamiques avec application au cas particulier de langages LISPiens. Thèse de doctorat en science, Université de Paris-sud, Orsay, 28 June 1988.Google Scholar
  28. [vEK76]
    M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the Association for Computing Machinary, 23(4):733–742, October 1976.Google Scholar
  29. [vG90]
    A. van Gelder. Deriving constraints among argument sizes in logic programs. In Proceedings of the 9 ACM Symposium on Principles of Database Systems, pages 47–60, Nashville, Tennesse, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Patrick Cousot
    • 1
  • Radhia Cousot
    • 2
  1. 1.LIENS, DMI, école Normale SupérieureParis cedex 05France
  2. 2.LIX, école PolytechniquePalaiseau cedexFrance

Personalised recommendations