Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Programming Language Implementation and Logic Programming (PLILP 1992)

Part of the book series: Lecture Notes in Computer Science ((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).

This work was supported in part by Esprit BRA action 3124 “Sémantique”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky and G. Hankin, editors. Abstract Interpretation of Declarative Languages. Computers and their Applications. Ellis Horwood, Chichester, U.K., 1987.

    Google Scholar 

  2. 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. 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. 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. F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 1992. (to appear).

    Google Scholar 

  6. 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. 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. 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. 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. 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. 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. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 1992. (to appear).

    Google Scholar 

  13. 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. 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. 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. 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. 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. P. Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30:165–190, 1989.

    Google Scholar 

  19. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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 

Download references

Author information

Authors and Affiliations

  1. LIENS, DMI, école Normale Supérieure, 45, rue d'Ulm, 75230, Paris cedex 05, France

    Patrick Cousot

  2. LIX, école Polytechnique, 91128, Palaiseau cedex, France

    Radhia Cousot

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radhia Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Maurice Bruynooghe Martin Wirsing

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cousot, P., Cousot, R. (1992). Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds) Programming Language Implementation and Logic Programming. PLILP 1992. Lecture Notes in Computer Science, vol 631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55844-6_142

Download citation

  • DOI: https://doi.org/10.1007/3-540-55844-6_142

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55844-6

  • Online ISBN: 978-3-540-47297-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation