Article

Free access

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

Authors:

Patrick Cousot,

Radhia CousotAuthors Info & Claims

POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 238 - 252

https://doi.org/10.1145/512950.512973

Published: 01 January 1977 Publication 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.

[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]

Henderson{75}. Finite state modelling in program development. Proc. Int. Conf. on Reliable Soft., Los Angeles, 221-227.

Digital 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.).

Digital Library

[7]

Hoare{67}. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct.), 576-580.

Digital Library

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

Digital Library

[11]

Katz and Manna{76}. Logical analysis of programs. Comm. ACM 19, 4(April), 188-206.

Digital 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.).

Digital Library

[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]

Manna and Shamir{75}. A new approach to recursive programs. Tech. Rep. CS-75-539, Comp. Sc. Dep., Stanford U.

Digital 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).

[18]

Naur{65}. Checking of operand types in ALGOL compilers, BIT 5, 151-163.

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

[20]

Schwartz{75}. Automatic data structure choice in a language of very high level. Comm. ACM 18, 12 (Dec.), 722-728.

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

[22]

Scott and Strachey{71}. Towards a mathematical semantics for computer languages. Tech. Mon. PRG-6, Oxford U. Comp. Lab.

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

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

[25]

Sintzoff{76}. Eliminating blind alleys from backtrack programs. Proc. of the third Int. Coll. on Automata, Languages and Programming, Edinburgh, (July).

[26]

Sites{74}. Proving that computer programs terminate cleanly. Ph.D. Th., Comp. Sc. Dep., Stanford U., (May).

Digital Library

[27]

Tarjan{75}. Solving path problems on directed graphs. Tech. Rep. CS-75-528, Comp. Sc. Dep., Stanford U.

Digital Library

[28]

Tarjan{76}. Iterative algorithms for global flow analysis. Tech. Rep. CS-76-547, Comp. Sc. Dep., Stanford U.

Digital Library

[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.)

Digital Library

[33]

Wegbreit{76}. Verifying program performance, J. ACM, 23, 4, (Oct.), 691-699.

Digital Library

Cited By

Susan S(2024)Leveraging Slither and Interval Analysis to build a Static Analysis ToolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.410.10410(150-166)Online publication date: 31-Oct-2024
https://doi.org/10.4204/EPTCS.410.10
Ge XFang CLi XSun WWu DZhai JLin SZhao ZLiu YChen Z(2024)Machine Learning for Actionable Warning Identification: A Comprehensive SurveyACM Computing Surveys10.1145/369635257:2(1-35)Online publication date: 19-Sep-2024
https://dl.acm.org/doi/10.1145/3696352
Fischer TFalk H(2024)Towards Analysing Cache-Related Preemption Delay in Non-Inclusive Cache HierarchiesACM Transactions on Embedded Computing Systems10.1145/369576824:1(1-37)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1145/3695768
Show More Cited By

Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
1. Theory of computation
  1. Semantics and reasoning

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 languages

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

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

Conference Chairs:
Robert M. Graham
University of Massachusetts, Amherst, Massachusetts
,
Michael A. Harrison
University of California, Berkeley, California
,
Program Chair:
Ravi Sethi
Bell Laboratories, Murray Hill, New Jersey

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1977

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '77 Paper Acceptance Rate 25 of 105 submissions, 24%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4,490
Total Citations
View Citations
12,674
Total Downloads

Downloads (Last 12 months)1,828
Downloads (Last 6 weeks)224

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Susan S(2024)Leveraging Slither and Interval Analysis to build a Static Analysis ToolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.410.10410(150-166)Online publication date: 31-Oct-2024
https://doi.org/10.4204/EPTCS.410.10
Ge XFang CLi XSun WWu DZhai JLin SZhao ZLiu YChen Z(2024)Machine Learning for Actionable Warning Identification: A Comprehensive SurveyACM Computing Surveys10.1145/369635257:2(1-35)Online publication date: 19-Sep-2024
https://dl.acm.org/doi/10.1145/3696352
Fischer TFalk H(2024)Towards Analysing Cache-Related Preemption Delay in Non-Inclusive Cache HierarchiesACM Transactions on Embedded Computing Systems10.1145/369576824:1(1-37)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1145/3695768
Park JLaddad SBali DZhang WShenker SZaharia MFilkov VRay BZhou M(2024)Everything Everywhere All At Once: Efficient Cross-Service Program Analysis with OverSeerProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering Workshops10.1145/3691621.3694937(82-87)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691621.3694937
Distefano DMarescotti MAhs CCela SSampaio GGrigore RHajdu AKapus TMao KSuzanne TFilkov VRay BZhou M(2024)Enhancing Compositional Static Analysis with Dynamic AnalysisProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695599(2121-2129)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695599
Huang ZRavi SWang CFilkov VRay BZhou M(2024)Discovering Likely Program Invariants for Persistent MemoryProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695544(1795-1807)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695544
Wang ZYang LChen MBu YLi ZWang QQin SYi XYin JFilkov VRay BZhou M(2024)Parf: Adaptive Parameter Refining for Abstract InterpretationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695487(1082-1093)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695487
Yoo JErnst MJust RFilkov VRay BZhou M(2024)Verifying the Option Type with Rely-Guarantee ReasoningProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695036(367-380)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695036
Kaindlstorfer DIsychev AWüstholz VChristakis MFilkov VRay BZhou M(2024)Interrogation Testing of Program Analyzers for Soundness and Precision IssuesProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695034(319-330)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695034
Böck MSchröder MCito JFilkov VRay BZhou M(2024)Language-Agnostic Static Analysis of Probabilistic ProgramsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695031(78-90)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695031
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents