article

Free access

Making abstract interpretations complete

Authors:

Roberto Giacobazzi,

Francesco Ranzato,

Francesca ScozzariAuthors Info & Claims

Journal of the ACM (JACM), Volume 47, Issue 2

Pages 361 - 416

https://doi.org/10.1145/333979.333989

Published: 01 March 2000 Publication History

Abstract

Completeness is an ideal, although uncommon, feature of abstract interpretations, formalizing the intuition that, relatively to the properties encoded by the underlying abstract domains, there is no loss of information accumulated in abstract computations. Thus, complete abstract interpretations can be rightly understood as optimal. We deal with both pointwise completeness, involving generic semantic operations, and (least) fixpoint completeness. Completeness and fixpoint completeness are shown to be properties that depend on the underlying abstract domains only. Our primary goal is then to solve the problem of making abstract interpretations complete by minimally extending or restricting the underlying abstract domains. Under the weak and reasonable hypothesis of dealing with continuous semantic operations, we provide constructive characterizations for the least complete extensions and the greatest complete restrictions of abstract domains. As far as fixpoint completeness is concerned, for merely monotone semantic operators, the greatest restrictions of abstract domains are constructively characterized, while it is shown that the existence of least extensions of abstract domains cannot be, in general, guaranteed, even under strong hypotheses. These methodologies, which in finite settings give rise to effective algorithms, provide advanced formal tools for manipulating and comparing abstract interpretations, useful both in static program analysis and in semantics design. A number of examples illustrating these techniques are given.

References

[1]

ABRAMSKY, S., AND JUNG, A. 1994. Domain theory. In Handbook of Logic in Computer Science, Volume 3. S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, Ed. Clarendon Press, Oxford, U.K., pp. 1-168.]]

[2]

AMATO, G., AND LEVI, G. 1997. Properties of the lattice of observables in logic programming. In Proceedings of the Italian-Portuguese-Spanish Joint Conference on Declarative Programming (APPI/I- GULP-PRODE '97). pp. 175-187.]]

[3]

APT, K. R., AND PLOTKIN, G.D. 1986. Countable nondeterminism and random assignment. J. ACM 33, 4, 724-767.]]

[4]

ARMSTRONG, T., MARRIOTT, K., SCHACHTE, P., AND SONDERGAARD, H. 1998. Two classes of Boolean functions for dependency analysis. Sci. Comput. Program 31, 1, 3-45.]]

[5]

BAGNARA, R., HILL, P. M., AND ZAFFANELLA, E. 1997. Set-sharing is redundant for pair sharing. In Proceedings of the 4th International Static/inalysis Symposium (S/tS '97), P. Van Hentenryck, Ed., Lecture Notes in Computer Science, vol. 1302. Springer-Verlag, New York, pp. 53-67.]]

[6]

BARBUTI, R., GIACOBAZZI, R., AND LEVI, G. 1993. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 15, 1, 133-181.]]

[7]

BIRKHOFF, G. 1967. Lattice Theory. AMS Colloquium Publication, 3rd edition, AMS, Providence, R.I.]]

[8]

BURN, G. L., HANKIN, C. L., AND ABRAMSKY, S. 1986. Strictness analysis of higher-order functions. Sci. Comput. Program. 7, 249-278.]]

[9]

CASEAU, Y. 1991. Abstract interpretation of constraints on order-sorted domains. In Proceedings of the 1991 International Logic Programming Symposium (ILPS '91), V. Saraswat and K. Ueda, Eds., The MIT Press, Cambridge, Mass., pp. 435-452.]]

[10]

CLARKE, E. M., GRUMBERG, 0., AND LONG, D.E. 1994. Model checking and abstraction./ICM Trans. Program. Lang. Syst. 16, 5, 1512-1542.]]

[11]

CLEAVELAND, R., IYER, P., AND YANKELEVICH, D. 1995. Optimality in abstractions of model checking. In Proceedings of the 2nd International Static Analysis Symposium (S/tS '95), A. Mycroft, Ed. Lecture Notes in Computer Science, vol. 983. Springer-Verlag, New York, pp. 51-63.]]

[12]

CLEAVELAND, R., AND RIELY, J. 1994. Testing-based abstractions for value-passing systems. In Proceedings of the 5th International Conference on Concurrency Theory (CONCUR '94), B. Jonsson and J. Parrow, Eds. Lecture Notes in Computer Science, vol. 836. Springer-Verlag, New York, pp. 417-432.]]

[13]

CODISH, M., DAMS, D., AND YARDENI, E. 1994a. Bottom-up abstract interpretation of logic programs. Theor. Comput. Sci. 124, 1, 93-126.]]

[14]

CODISH, M., FALASCHI, M., AND MARRIOTT, K. 1994b. Suspension analyses for concurrent logic programs. ACM Trans. Program. Lang. Syst. 16, 3, 649-686.]]

[15]

COLBY, C. 1997. Accumulated imprecision in abstract interpretation. In Proceedings of the 1st ACM Workshop on Automatic Analysis of Software (A/tS '97), R. Cleaveland and D. Jackson, Eds. ACM, New York, pp. 77-89.]]

[16]

COMINI, M., AND LEVI, G. 1994. An algebraic theory of observables. In Proceedings of the 1994 International Logic Programming Symposium (ILPS '94), M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., pp. 172-186.]]

[17]

COMINI, M., LEVI, G., AND MEO, M.C. 1995. Compositionality of SLD-derivations and their abstractions. In Proceedings of the 1995 International Logic Programming Symposium (ILPS '95), J. Lloyd, Ed. The MIT Press, Cambridge, Mass., pp. 561-575.]]

[18]

CORTESI, A., FILIE, G., GIACOBAZZI, R., PALAMIDESSI, C., AND RANZATO, F. 1997. Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst. 19, 1, 7-47.]]

[19]

CORTESI, A., FILI~, G., AND WINSBOROUGH, W. 1996. Optimal groundness analysis using propositional logic. J. Logic Program. 27, 2, 137-167.]]

[20]

CORTESI, A., FILE, G., AND WINSBOROUGH, W. i998. The quotient of an abstract interpretation. Theor. Comput. Sci. 202, 1-2, 163-192.]]

[21]

CORTESI, A., LE CHARLIER, B., AND VAN HENTENRYCK, P. i995. Evaluation of the domain Prop. J. Logic Program. 23, 3, 237-278.]]

[22]

COUSOT, P. 1978. Mdthodes it6ratives de construction et d'approximation de points fixes d'op6rateurs monotones sur un treillis, analyse sdmantique des programmes. Ph.D. dissertation. Universit6 Scientifique et M6dicale de Grenoble, Grenoble, France.]]

[23]

COUSOT, P. 1996a. Abstract interpretation. ACM Comput. Surv. 28, 2, 324-328.]]

[24]

COUSOT, P. 1996b. Program analysis: The abstract interpretation perspective. ACM Comput. Surv. 28A, 4es, 165-es.]]

[25]

COUSOT, P. 1997. Types as abstract interpretations (Invited Paper). In Conference Record of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97) (Paris, France, Jan. 15-17). ACM Press, New York, pp. 316-331.]]

[26]

COUSOT, P. 2000. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret. Comput. Sci., to appear.]]

[27]

COUSOT, P. AND COUSOT, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming. Dunod, Paris, pp. 106-130.]]

[28]

COUSOT, P., AND COUSOT, R. 1997. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL '77). ACM Press, New York, pp. 238-252.]]

[29]

COUSOT, P., AND COUSOT, R. 1979. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL '79). ACM Press, New York, pp. 269-282.]]

[30]

COUSOT, P., AND COUSOT, R. 1992a. Abstract interpretation and application to logic programs. J. Logic Program. 13, 2-3, 103-179.]]

[31]

COUSOT, P., AND COUSOT, R. 1992b. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '92) (Albuquerque, N.M., Jan. 19-22). ACM Press, New York, pp. 83-94.]]

[32]

COUSOT, P., AND COUSOT, R. 1993. Galois connection based abstract interpretation for strictness analysis (Invited Paper). In Proceedings of the International Conference on Formal Methods in Programming and Their Applications (FMPA '93), D. BjOrner, M. Broy, and I. Pottosin, Eds. Lecture Notes in Computer Science, Vol. 735. Springer-Verlag, New York, pp. 98-127.]]

[33]

COUSOT, P., AND COUSOT, R. 1995. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form (Invited Paper). In Proceedings of the 7th International Conference on Computer Aided Verification (CAV '95), P. Wolper, Ed. Lecture Notes in Computer Science, vol. 939. Springer-Verlag, New York, pp. 293-308.]]

[34]

COUSOT, P., AND COUSOT, R. 1997. Abstract interpretation of algebraic polynomial systems. In Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST '97), M. Johnson, Ed. Lecture Notes in Computer Science. Springer-Verlag, New York, pp. 138-154.]]

[35]

DAMS, D. 1996. Abstract interpretation and partition refinement for model checking. Ph.D. dissertation. Eindhoven Univ. of Technology, Eindhoven, The Netherlands.]]

[36]

DAMS, D., GERTH, R., AND GRUMBERG, 0. 1997. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19, 2, 253-291.]]

[37]

DAVEY, B. A., AND PRIESTLEY, H.A. 1990. Introduction to Lattices and Order. Cambridge University Press, Cambridge, U.K.]]

[38]

DE BAKKER, J. W., MEYER, J.-J. C., AND ZUCKER, J.I. 1983. On infinite computations in denotational semantics. Theoret. Comput. Sci. 26, 1-2, 53-82.]]

[39]

DEBRAY, S.K. 1995. On the complexity of dataflow analysis of logic programs. ACM Trans. Program. Lang. Syst. 17, 2, 331-365.]]

[40]

DEUTSCH, A. 1997. On the complexity of escape analysis. In Conference Record of the 24th ACM Symposium on Principles of Programming Languages (POPL '97) (Paris, France, Jan. 15-17). ACM Press, New York, pp. 358-371.]]

[41]

FALASCHI, M., LEVI, G., MARTELLI, M., AND PALAMIDESSI, C. 1989. Declarative modeling of the operational behavior of logic languages. Theoret. Comput. Sci. 69, 3, 289-318.]]

[42]

FILth, G., GIACOBAZZI, R., AND RANZATO, F. 1996. A unifying view of abstract domain design. ACM Comput. Surv. 28, 2, 333-336.]]

[43]

FILITH, G., AND RANZATO, F. 1999. The powerset operator on abstract interpretations. Theoret. Comput. Sci. 222, 1-2, 77-111.]]

[44]

GIACOBAZZI, R. 1996. "Optimal" collecting semantics for analysis in a hierarchy of logic program semantics. In Proceedings of the 13th International Symposium on Theoretical Aspects of Computer Science (STACS '96), C. Puech and R. Reischuk, Eds. Lecture Notes in Computer Science, vol. 1046. Springer-Verlag, New York, pp. 503-514.]]

[45]

GIACOBAZZI, R., AND RANZATO, F. 1997. Refining and compressing abstract domains. In Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP '97), P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, Eds. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, New York, pp. 771-781.]]

[46]

GIACOBAZZI, R., AND RANZATO, F. 1998a. Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program 32, 1-3, 177-210.]]

[47]

GIACOBAZZI, R., AND RANZATO, F. 1998b. Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Info. Comput. 145, 2, 153-190.]]

[48]

GIACOBAZZI, R., RANZATO, F., AND SCOZZARI, F. 1998. Complete abstract interpretations made constructive. In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS '98), L. Brim, J. Gruska, and J. Zlatugka, Eds. Lecture Notes in Computer Science, vol. 1450. Springer-Verlag, New York, pp. 366-377.]]

[49]

GRAF, S. 1999. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distrib. Comput. 12, 2-3, 75-90.]]

[50]

HERMENEGILDO, M., WARREN, D. S., AND DEBRAY, S.K. 1992. Global flow analysis as a practical compilation tool. J. Logic Program. 13, 4, 349-366.]]

[51]

JACOBS, D., AND LANGEN, A. 1992. Static analysis of logic programs for independent AND- parallelism. J. Logic Program. 13, 2-3, 154-165.]]

[52]

KING, A., SMAUS, J., AND HILL, P. 1999. Quotienting Share for dependency analysis. In Proceedings of the 8th European Symposium on Programming (ESOP '99), S. D. Swierstra, Ed. Lecture Notes in Computer Science, vol. 1576. Springer-Verlag, New York, pp. 59-73.]]

[53]

LASSEZ, J.-L., MAHER, M.J., AND MARRIOTT, K. 1988. Unification revisited. In Foundations of Deductive Databases and Logic Programming, J. Minker, Ed. Morgan-Kaufmann, Los Altos, Calif., pp. 587-625.]]

[54]

LOISEAUX, C., GRAF, S., SIFAKIS, J., BOUAJJANI, A., AND BENSALEM, S. 1995. Property preserving abstractions for the verification of concurrent systems. Formal Methods SysL Des. 6, 11-44.]]

[55]

MARRIOTT, K., AND SONDERGAARD, H. 1993. Precise and efficient groundness analysis for logic programs. ACM Lett. Program. Lang. Syst. 2, 1-4, 181-196.]]

[56]

MARRIOTT, K., SONDERGAARD, H., AND JONES, N.D. 1994. Denotational abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 16, 3, 607-648.]]

[57]

MATHEMATICS OF PROGRAM CONSTRUCTION GROUP. 1995. Fixed-point calculus. Inform. Process. Lett. 53, 3, 131-136.]]

[58]

MONSUEZ, B. 1995. System F and abstract interpretation. In Proceedings of the 2nd International Static Analysis Symposium (SAS '95), A. Mycroft, Ed. Lecture Notes in Computer Science, vol. 983. Springer-Verlag, New York, pp. 279-295.]]

[59]

MYCROFT, A. 1980. The theory and practice of transforming call-by-need into call-by-value. In Proceedings of the 4th International Symposium on Programming, B. Robinet, Ed. Lecture Notes in Computer Science, vol. 83. Springer-Verlag, New York, pp. 269-281.]]

[60]

MYCROFT, A. 1981. Abstract interpretation and optimising transformations for applicative programs. Ph.D. dissertation. CST-15-81, Univ. of Edinburgh, Edinburgh, Scotland.]]

[61]

MYCROFT, A. 1993. Completeness and predicate-based abstract interpretation. In Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM '93). ACM, New York, pp. 179-185.]]

[62]

{0RBA~K, P. 1995. Can you trust your data? In Proceedings of the 6th International Joint Conference CAAP/FASE, Theory and Practice of Software Development (TAPSOFT '95), P. Mosses, M. Nielsen, and M. Schwartzbach, Eds. Lecture Notes in Computer Science, vol. 915. Springer-Verlag, New York, pp. 575-589.]]

[63]

{0RB~EK, P., AND PALSBERG, J. 1997. Trust in the lambda-calculus. J. Funct. Program. 7, 6, 557-591.]]

[64]

PARK, Y., AND GOLDBER6, B. 1992. Escape analysis on lists. In Proceedings of the 1992 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '92) (San Francisco, Calif., June 17-19). ACM, New York, pp. 116-127.]]

[65]

PLAISTED, D. 1981. Theorem proving with abstraction. Artif. Intell. 16, 47-108.]]

[66]

RANZATO, F. 1999. Closures on CPOs form complete lattices. Infor. Comput., 152, 2, 236-249.]]

[67]

REDDY, U. S., AND KAMIN, S.N. 1993. On the power of abstract interpretation. Comput. Lang. 19, 2, 79-89.]]

[68]

SEKAR, R.C., MISHRA, P., AND RAMAKRISHNAN, I.V. 1997. On the power and limitation of strictness analysis. J. ACM 44, 3, 505-525.]]

[69]

STEFFEN, B. 1987. Optimal run time optimization proved by a new look at abstract interpretation. In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT '87), H. Ehrig, R.A. Kowalski, G. Levi, and U. Montanari, Eds. Lecture Notes in Computer Science, vol. 249. Springer-Verlag, New York, pp. 52-68.]]

[70]

STEFFEN, B. 1989. Optimal data flow analysis via observational equivalence. In Proceedings of the 14th International Symposium on Mathematical Foundations of Computer Science (MFCS '89), A. Kreczmar and G. Mirkowska, Eds. Lecture Notes in Computer Science, vol. 379. Springer-Verlag, New York, pp. 492-502.]]

[71]

STEFFEN, B., JAY, C. B., AND MENDLER, M. 1992. Compositional characterization of observable program properties. RAIRO Inform. Thdor. Appl. 26, 5, 403-424.]]

[72]

VAN ROY, P., AND DESPAIN, A.M. 1990. The benefits of global dataflow analysis for an optimizing Prolog compiler. In Proceedings of the 1990 North American Conference on Logic Programming (NACLP '90) S.K. Debray and M. Hermenegildo, Eds. The MIT Press, Cambridge, Mass., pp. 501-515.]]

[73]

VENET, A. 1996. Abstract interpretation of the w-calculus. In Proceedings of the 5th LOMAPS Meeting on Analysis and Verification of High-Level Concurrent Languages, M. Dam, Ed. Lecture Notes in Computer Science, vol. 1192. Springer-Verlag, New York, pp. 51-75.]]

[74]

VON KARGER, B. 1998. Temporal algebra. Math. Struct. Comput. Sci. 8, 3, 277-320. WARD, M. 1942. The closure operators of a lattice. Ann. Math. 43, 2, 191-196.]]

Cited By

Giacobazzi RRanzato F(2025)The Best of Abstract InterpretationsProceedings of the ACM on Programming Languages10.1145/37048829:POPL(1355-1385)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704882
Mastroeni I(2025)Abstract domain adequacyInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00774-x26:6(747-765)Online publication date: 2-Jan-2025
https://doi.org/10.1007/s10009-024-00774-x
Mastroeni I(2025)Abstract Local CompletenessVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82703-7_1(3-25)Online publication date: 23-Jan-2025
https://doi.org/10.1007/978-3-031-82703-7_1
Show More Cited By

Index Terms

Making abstract interpretations complete
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Making abstract interpretations complete
The Best of Abstract Interpretations

We study “the best of abstract interpretations”, that is, the best possible abstract interpretations of programs. Abstract interpretations are inductively defined by composing abstract transfer functions for the basic commands, such as assignments and ...
Inductive definitions, semantics and abstract interpretations
POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can ...

Comments

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 47, Issue 2

March 2000

192 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/333979

Issue’s Table of Contents

Copyright © 2000 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2000

Published in JACM Volume 47, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

241
Total Citations
View Citations
1,522
Total Downloads

Downloads (Last 12 months)197
Downloads (Last 6 weeks)29

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Giacobazzi RRanzato F(2025)The Best of Abstract InterpretationsProceedings of the ACM on Programming Languages10.1145/37048829:POPL(1355-1385)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704882
Mastroeni I(2025)Abstract domain adequacyInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00774-x26:6(747-765)Online publication date: 2-Jan-2025
https://doi.org/10.1007/s10009-024-00774-x
Mastroeni I(2025)Abstract Local CompletenessVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82703-7_1(3-25)Online publication date: 23-Jan-2025
https://doi.org/10.1007/978-3-031-82703-7_1
Giacobazzi RMastroeni IPerantoni E(2024)Adversities in Abstract Interpretation - Accommodating Robustness by Abstract InterpretationACM Transactions on Programming Languages and Systems10.1145/364930946:2(1-31)Online publication date: 24-Feb-2024
https://dl.acm.org/doi/10.1145/3649309
Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
AMATO GSCOZZARI F(2024)Optimal Matching for Sharing and Linearity AnalysisTheory and Practice of Logic Programming10.1017/S1471068424000152(1-27)Online publication date: 22-Nov-2024
https://doi.org/10.1017/S1471068424000152
Baldan PKönig BPadoan T(2024)Systems of fixpoint equationsInformation and Computation10.1016/j.ic.2024.105233301:PAOnline publication date: 1-Dec-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105233
Babu MLemerre MBardin SMarion J(2024)Trace Partitioning as an Optimization ProblemStatic Analysis10.1007/978-3-031-74776-2_2(26-60)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74776-2_2
Negrini LArceri VCortesi AFerrara P(2024)tarsisJournal of Software: Evolution and Process10.1002/smr.264736:8Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1002/smr.2647
Bruni RGiacobazzi RGori RRanzato F(2023)A Correctness and Incorrectness Program LogicJournal of the ACM10.1145/358226770:2(1-45)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582267
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 Article

Figures

Tables

Media

View Issue’s Table of Contents