Abstract cofibered domains: Application to the alias analysis of untyped programs

  • Arnaud Venet
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


We present a class of domains for Abstract Interpretation, the cofibered domains, that are obtained by “glueing∝ a category of partially ordered sets together. The internal structure of these domains is well suited to the compositional design of approximations and widening operators, and we give generic methods for performing such constructions. We illustrate the interest of these domains by developing an alias analysis of untyped programs handling structured data. The results obtained with this analysis are comparable in accuracy to those obtained with the most powerful alias analyses existing for typed languages.


Widening Operator Abstract Interpretation Abstract Domain Affine Subspace Abstract Semantic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Bou92]
    F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4), 1992.Google Scholar
  2. [BW90]
    M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1990.Google Scholar
  3. [CC76]
    P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the 2 nd International Symposium on Programming, pages 106–130, Paris, 1976. Dunod.Google Scholar
  4. [CC77]
    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 4 th ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, U.S.A., 1977.Google Scholar
  5. [CC79]
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th POPL. ACM Press, 1979.Google Scholar
  6. [CC92a]
    P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511–547, August 1992.Google Scholar
  7. [CC92b]
    P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, August 1992. Springer-Verlag, Berlin, Germany, 1992.Google Scholar
  8. [CC95]
    P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Conference Record of FPCA '95. ACM Press, 1995.Google Scholar
  9. [CH78]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th POPL. ACM Press, 1978.Google Scholar
  10. [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 des programmes. PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.Google Scholar
  11. [Cou96]
    P. Cousot. Abstract interpretation in categorical form. To appear, 1996.Google Scholar
  12. [Deu92a]
    A. Deutsch. Operational models of programming languages and representations of relations on regular languages with application to the static determination of dynamic aliasing properties of data. PhD thesis, University Paris VI (France), 1992.Google Scholar
  13. [Deu92b]
    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, pages 2–13. IEEE Computer Society Press, Los Alamitos, California, U.S.A., 1992.Google Scholar
  14. [Deu94]
    A. Deutsch. Interprocedural may-alias analysis for pointers: beyond k-limiting. In ACM SIGPLAN'94 Conference on Programming Language Design and Implementation. ACM Press, 1994.Google Scholar
  15. [Gra89]
    P. Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30:165–190, 1989.Google Scholar
  16. [Gra91]
    P. Granger. Static analysis of linear congruence equalities among variables of a program. In TAPSOFT'91, volume 493. Lecture Notes in Computer Science, 1991.Google Scholar
  17. [Gra92]
    P. Granger. Improving the results of static analyses of programs by local decreasing iterations. In 12th Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science. Springer Verlag, 1992.Google Scholar
  18. [JM81]
    N. Jones and S. Muchnick. Flow analysis and optimization of lisp-like structures. In Program Flow Analysis: Theory and Applications, pages 102–131. Prentice Hall, 1981.Google Scholar
  19. [Jon81]
    H.B.M Jonkers. Abstract storage structures. In De Bakker and Van Vliet, editors, Algorithmic languages, pages 321–343. IFIP, 1981.Google Scholar
  20. [Kar76]
    M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133–151, 1976.Google Scholar
  21. [Kel74]
    G.M. Kelly. On clubs and doctrines. In A. Dold and B. Eckmann, editors, Category seminar, volume 420 of Lecture Notes in Mathematics, pages 181–256. Springer Verlag, 1974.Google Scholar
  22. [Ven96]
    A. Venet. Abstract interpretation of the π-calculus. 5th LOMAPS Workshop on Analysis and Verification of High-Level Concurrent Languages, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Arnaud Venet
    • 1
  1. 1.école PolytechniqueLIXPalaiseauFrance

Personalised recommendations