skip to main content
10.1145/512950.512973acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article
Free Access

Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

Authors Info & Claims
Published:01 January 1977Publication History

ABSTRACT

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).

References

  1. Birkhoff{6}. Lattice theory. Amer. Math. Soc. Col. Pub., XXV, Rev. ed.Google ScholarGoogle Scholar
  2. Cousot{76}. Static determination of dynamic properties of programs. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear (April).Google ScholarGoogle Scholar
  3. Cousot{76'}. Static determination of dynamic properties of generalized type unions. Submitted for publication. (Sept.)Google ScholarGoogle Scholar
  4. Floyd{67}. Assigning meanings to programs. Proc. Symp. in Appl. Math. Vol. 19. Mathematical Aspects of Computer Science, (J. Schwartz, ed.) AMS, Providence, R.I., 19-32.Google ScholarGoogle Scholar
  5. Henderson{75}. Finite state modelling in program development. Proc. Int. Conf. on Reliable Soft., Los Angeles, 221-227. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Hewitt et al.{73}. Actor induction and meta-evaluation. Conf. Rec. of the First ACM Symp. on Principles of Programming Languages, Boston, 153-168, (Oct.). Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Hoare{67}. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct.), 576-580. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Hoare and Lauer{74}. Consistent and Complementary formal theories of the semantics of programming languages. Acts Inf. 3, 135-153.Google ScholarGoogle Scholar
  9. Kam and Ullman{75}. Monotone data flow analysis frameworks. TR.169, C.S. Lab., Princeton Univ.Google ScholarGoogle Scholar
  10. Karr{76}. Affine relationships among variables of a program. Acta Inf. 6, 133-151.Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Katz and Manna{76}. Logical analysis of programs. Comm. ACM 19, 4(April), 188-206. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Kildall{73}.A unified approach to global program optimization. Conf. Rec. of the First ACM Symp. on Principles of Programming Languages, Boston, 194-206, (Oct.). Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Kleene{52}. Introduction to metamathematics. Van Nostrand, New York.Google ScholarGoogle Scholar
  14. Ligler{75}. Surface properties of programming language constructs. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.), IRIA, France.Google ScholarGoogle Scholar
  15. Mac Neille{37}. Partially ordered sets. Trans. Amer. Math. Soc., 42, 416-460.Google ScholarGoogle ScholarCross RefCross Ref
  16. Manna and Shamir{75}. A new approach to recursive programs. Tech. Rep. CS-75-539, Comp. Sc. Dep., Stanford U. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Morel and Renvoise{76}. Une méthode globale d'élimination des redondances partielles. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear. (April).Google ScholarGoogle Scholar
  18. Naur{65}. Checking of operand types in ALGOL compilers, BIT 5, 151-163.Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Park{69}. Fixpoint induction and proofs of program properties. Machine Intelligence 5, (B. Meltzer and D. Michie, eds.), Edinburgh U. Press, 59-78.Google ScholarGoogle Scholar
  20. Schwartz{75}. Automatic data structure choice in a language of very high level. Comm. ACM 18, 12 (Dec.), 722-728. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Scott{71}. The lattice of flow diagrams. Symp. on Semantics of Programming Languages. Springer-Verlag Lecture Notes in Math. (E. Engeler, ed.), Vol. 188.Google ScholarGoogle Scholar
  22. Scott and Strachey{71}. Towards a mathematical semantics for computer languages. Tech. Mon. PRG-6, Oxford U. Comp. Lab.Google ScholarGoogle Scholar
  23. Sintzoff{72}. Calculating properties of programs by valuations on specific models. Proc. ACM conf. on Proving Assertions About Programs. SIGPLAN Notices 7, 1, 203-207. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Sintzoff{75}. Vérifications d'assertions pour les fonctions utilisables comme valeurs affectant des variables extérieures. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.). IRIA. France.Google ScholarGoogle Scholar
  25. Sintzoff{76}. Eliminating blind alleys from backtrack programs. Proc. of the third Int. Coll. on Automata, Languages and Programming, Edinburgh, (July).Google ScholarGoogle Scholar
  26. Sites{74}. Proving that computer programs terminate cleanly. Ph.D. Th., Comp. Sc. Dep., Stanford U., (May). Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Tarjan{75}. Solving path problems on directed graphs. Tech. Rep. CS-75-528, Comp. Sc. Dep., Stanford U. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Tarjan{76}. Iterative algorithms for global flow analysis. Tech. Rep. CS-76-547, Comp. Sc. Dep., Stanford U. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Tarski{55}. A lattice theoretical fixpoint theorem and its applications. Pacific journal of Math. 5, 285-309.Google ScholarGoogle Scholar
  30. Tenenbaum{74}. Type determination for very high level languages. NSO-3, Courant Inst. of Math. Sc., New York U., (Oct.).Google ScholarGoogle Scholar
  31. Ullman{75}. Data flow analysis. Tech. Rep. 179, Dep. of Elec. Eng., Comp. Sc. Lab., Princeton U., (March).Google ScholarGoogle Scholar
  32. Wegbreit{75}. Property extraction in well-founded property sets. IEEE trans. on Soft. Eng., Vol . SE-1, No. 3, (Sept.) Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. Wegbreit{76}. Verifying program performance, J. ACM, 23, 4, (Oct.), 691-699. Google ScholarGoogle ScholarDigital LibraryDigital Library
  1. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in
    • Published in

      cover image ACM Conferences
      POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages
      January 1977
      280 pages
      ISBN:9781450373500
      DOI:10.1145/512950

      Copyright © 1977 ACM

      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 1 January 1977

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • Article

      Acceptance Rates

      POPL '77 Paper Acceptance Rate25of105submissions,24%Overall Acceptance Rate824of4,130submissions,20%

      Upcoming Conference

      POPL '25

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader