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

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.
• 2: Cousot{76}. Static determination of dynamic properties of programs. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear (April).
• 3: Cousot{76'}. Static determination of dynamic properties of generalized type unions. Submitted for publication. (Sept.)
• 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.
• 5: Peter Henderson, Finite state modelling in program development, Proceedings of the international conference on Reliable software, p.221-227, April 21-23, 1975, Los Angeles, California
• 6: Carl Hewitt , Peter Bishop , Irene Greif , Brian Smith , Todd Matson , Richard Steiger, Actor induction and meta-evaluation, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.153-168, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512942]
• 7: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 8: Hoare and Lauer{74}. Consistent and Complementary formal theories of the semantics of programming languages. Acts Inf. 3, 135-153.
• 9: Kam and Ullman{75}. Monotone data flow analysis frameworks. TR.169, C.S. Lab., Princeton Univ.
• 10: Karr{76}. Affine relationships among variables of a program. Acta Inf. 6, 133-151.
• 11: Shmuel Katz , Zohar Manna, Logical analysis of programs, Communications of the ACM, v.19 n.4, p.188-206, April 1976 [doi>10.1145/360032.360048]
• 12: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 13: Kleene{52}. Introduction to metamathematics. Van Nostrand, New York.
• 14: Ligler{75}. Surface properties of programming language constructs. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.), IRIA, France.
• 15: Mac Neille{37}. Partially ordered sets. Trans. Amer. Math. Soc., 42, 416-460.
• 16: Z Manna , Adi Shamir, A new approach to recursive programs., Stanford University, Stanford, CA, 1975
• 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).
• 18: Naur{65}. Checking of operand types in ALGOL compilers, BIT 5, 151-163.
• 19: Park{69}. Fixpoint induction and proofs of program properties. Machine Intelligence 5, (B. Meltzer and D. Michie, eds.), Edinburgh U. Press, 59-78.
• 20: J. T. Schwartz, Automatic data structure choice in a language of very high level, Communications of the ACM, v.18 n.12, p.722-728, Dec. 1975 [doi>10.1145/361227.361235]
• 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.
• 22: Scott and Strachey{71}. Towards a mathematical semantics for computer languages. Tech. Mon. PRG-6, Oxford U. Comp. Lab.
• 23: Michel Sintzoff, Calculating properties of programs by valuations on specific models, Proceedings of ACM conference on Proving assertions about programs, p.203-207, January 06-07, 1972, Las Cruces, New Mexico, United States
• 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.
• 25: Sintzoff{76}. Eliminating blind alleys from backtrack programs. Proc. of the third Int. Coll. on Automata, Languages and Programming, Edinburgh, (July).
• 26: Richard Lee Sites, Proving that computer programs terminate cleanly., 1974
• 27: Robert E Tarjan, Solving path problems on directed graphs., Stanford University, Stanford, CA, 1975
• 28: Robert E Tarjan, Iterative algorithms for global flow analysis, Stanford University, Stanford, CA, 1976
• 29: Tarski{55}. A lattice theoretical fixpoint theorem and its applications. Pacific journal of Math. 5, 285-309.
• 30: Tenenbaum{74}. Type determination for very high level languages. NSO-3, Courant Inst. of Math. Sc., New York U., (Oct.).
• 31: Ullman{75}. Data flow analysis. Tech. Rep. 179, Dep. of Elec. Eng., Comp. Sc. Lab., Princeton U., (March).
• 32: Wegbreit{75}. Property extraction in well-founded property sets. IEEE trans. on Soft. Eng., Vol . SE-1, No. 3, (Sept.)
• 33: Ben Wegbreit, Verifying Program Performance, Journal of the ACM (JACM), v.23 n.4, p.691-699, Oct. 1976 [doi>10.1145/321978.321987]