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, …).
- Birkhoff{6}. Lattice theory. Amer. Math. Soc. Col. Pub., XXV, Rev. ed.Google Scholar
- Cousot{76}. Static determination of dynamic properties of programs. Programming Symp. Paris. Springer-Verlag Lecture Notes in Comp. Sc. to appear (April).Google Scholar
- Cousot{76'}. Static determination of dynamic properties of generalized type unions. Submitted for publication. (Sept.)Google Scholar
- 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 Scholar
- Henderson{75}. Finite state modelling in program development. Proc. Int. Conf. on Reliable Soft., Los Angeles, 221-227. Google ScholarDigital Library
- 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 ScholarDigital Library
- Hoare{67}. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct.), 576-580. Google ScholarDigital Library
- Hoare and Lauer{74}. Consistent and Complementary formal theories of the semantics of programming languages. Acts Inf. 3, 135-153.Google Scholar
- Kam and Ullman{75}. Monotone data flow analysis frameworks. TR.169, C.S. Lab., Princeton Univ.Google Scholar
- Karr{76}. Affine relationships among variables of a program. Acta Inf. 6, 133-151.Google ScholarDigital Library
- Katz and Manna{76}. Logical analysis of programs. Comm. ACM 19, 4(April), 188-206. Google ScholarDigital Library
- 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 ScholarDigital Library
- Kleene{52}. Introduction to metamathematics. Van Nostrand, New York.Google Scholar
- Ligler{75}. Surface properties of programming language constructs. Int. Symp. on Proving and Improving Programs, (G. Huet and G. Kahn, eds.), IRIA, France.Google Scholar
- Mac Neille{37}. Partially ordered sets. Trans. Amer. Math. Soc., 42, 416-460.Google ScholarCross Ref
- Manna and Shamir{75}. A new approach to recursive programs. Tech. Rep. CS-75-539, Comp. Sc. Dep., Stanford U. Google ScholarDigital Library
- 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 Scholar
- Naur{65}. Checking of operand types in ALGOL compilers, BIT 5, 151-163.Google ScholarDigital Library
- Park{69}. Fixpoint induction and proofs of program properties. Machine Intelligence 5, (B. Meltzer and D. Michie, eds.), Edinburgh U. Press, 59-78.Google Scholar
- Schwartz{75}. Automatic data structure choice in a language of very high level. Comm. ACM 18, 12 (Dec.), 722-728. Google ScholarDigital Library
- 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 Scholar
- Scott and Strachey{71}. Towards a mathematical semantics for computer languages. Tech. Mon. PRG-6, Oxford U. Comp. Lab.Google Scholar
- 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 ScholarDigital Library
- 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 Scholar
- Sintzoff{76}. Eliminating blind alleys from backtrack programs. Proc. of the third Int. Coll. on Automata, Languages and Programming, Edinburgh, (July).Google Scholar
- Sites{74}. Proving that computer programs terminate cleanly. Ph.D. Th., Comp. Sc. Dep., Stanford U., (May). Google ScholarDigital Library
- Tarjan{75}. Solving path problems on directed graphs. Tech. Rep. CS-75-528, Comp. Sc. Dep., Stanford U. Google ScholarDigital Library
- Tarjan{76}. Iterative algorithms for global flow analysis. Tech. Rep. CS-76-547, Comp. Sc. Dep., Stanford U. Google ScholarDigital Library
- Tarski{55}. A lattice theoretical fixpoint theorem and its applications. Pacific journal of Math. 5, 285-309.Google Scholar
- Tenenbaum{74}. Type determination for very high level languages. NSO-3, Courant Inst. of Math. Sc., New York U., (Oct.).Google Scholar
- Ullman{75}. Data flow analysis. Tech. Rep. 179, Dep. of Elec. Eng., Comp. Sc. Lab., Princeton U., (March).Google Scholar
- Wegbreit{75}. Property extraction in well-founded property sets. IEEE trans. on Soft. Eng., Vol . SE-1, No. 3, (Sept.) Google ScholarDigital Library
- Wegbreit{76}. Verifying program performance, J. ACM, 23, 4, (Oct.), 691-699. Google ScholarDigital Library
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
Recommendations
Abstract interpretation of resolution-based semantics
We extend the abstract interpretation point of view on context-free grammars by Cousot and Cousot to resolution-based logic programs and proof systems. Starting from a transition-based small-step operational semantics of Prolog programs (akin to the ...
Abstract Interpretation as Automated Deduction
Automata theory, algorithmic deduction and abstract interpretation provide the foundation behind three approaches to implementing program verifiers. This article is a first step towards a mathematical translation between these approaches. By extending ...
Temporal abstract interpretation
POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the @@@@-calculus, a generalization of the μ-calculus with new reversal and abstraction modalities ...
Comments