Skip to main content
SpringerLink
Log in

Prime factorizations of abstract domains using first-order logic

  • Abstrcet Interpretation
  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1139))

Included in the following conference series:

Abstract

A methodology is introduced based on first-order logic, for the design and decomposition of abstract domains for abstract interpretation. First, an assertion language is chosen that describes the properties of interest. Next, abstract domains are defined to be suitably chosen sets of assertions. Finally, computer representations of abstract domains are defined in the expected way, as isomorphic copies of their specification in the assertion language. In order to decompose abstract domains, the notion of prime (conjunctive) factorization of sets of assertions is introduced. We illustrate this approach by considering typical abstract domains for ground-dependency and aliasing analysis in logic programming.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt and E. Marchiori. Reasoning about Prolog programs: from Modes through types to assertions. In Formal Aspects of Computing, vol. 6A, pag. 743–764, 1994.

    Google Scholar 

  2. T. Armstrong, K. Marriott, P. Schachte and H. Søndergaard. Boolean Functions for Dependency Analysis: Algebraic Properties and Efficient Representation. Proc. SAS'94, B. Le Charlier ed., Springer-Verlag, LNCS 864, pp. 266–280, 1994.

    Google Scholar 

  3. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. Proc. POPL '79, pp. 269–282. ACM Press, 1979.

    Google Scholar 

  4. A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. Proc. SAS '95, A. Mycroft ed., LNCS Vol. 983, pp. 100–117. Springer-Verlag, 1995.

    Google Scholar 

  5. A. Cortesi, G. Filé, and W. Winsborough. Prop revised: propositional formula as abstract domain for groundness analysis. Proc. LICS '91, G. Kahn ed., pp. 322–327, 1991.

    Google Scholar 

  6. A. Cortesi, G. Filé, and W. Winsborough. Comparison of abstract interpretations. Proc. ICALP '92, W. Kuich, ed. LNCS Vol. 623, pp. 521–532. Springer-Verlag, 1992.

    Google Scholar 

  7. A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation. Technical Report 12/94, Dipartimento di Matematica Pura ed Applicata, Università di Padova, 1994.

    Google Scholar 

  8. P. Dart. On derived dependencies and connected databases. Journal of Logic Programming, 11(2):163–188, 1991.

    Google Scholar 

  9. S. Debray. On the Complexity of Dataflow Analysis of Logic Programs. Proc. ICALP '92, Springer Verlag, pp. 509–520, LNCS 623, 1992.

    Google Scholar 

  10. D. Jacobs and A. Langen. Static analysis of logic programs for independent AND-parallelism. Journal of Logic Programming, 13(2,3):154–165, 1992.

    Google Scholar 

  11. T.P. Jensen. Strictness Analysis in Logical Form. Proc. Conference on Functional Programming Languages and Computer Architectures, Springer Verlag, pp. 352–366, LNCS 523, 1991.

    Google Scholar 

  12. N.D. Jones and H. Søndergaard. A Semantics-Based Framework for the Abstract Interpretation of Prolog. Abstract Interpretation of Declarative Languages, eds. S. Abramsky and C. Hankin, Ellis Horwood, Chichester, U.K., pp. 123–142, 1987.

    Google Scholar 

  13. E. Marchiori. A Logic for Variable Aliasing in Logic Programs. Proc. ALP '94, G. Levi, M. Rodriguez-Artalejo eds., Springer Verlag, pp. 287–304, LNCS 850, 1994.

    Google Scholar 

  14. K. Marriott and H. Søndergaard. Notes for a tutorial on abstract interpretation of logic programs. North American Conference on Logic Programming, 1989.

    Google Scholar 

  15. K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM LoPLaS, 2(1–4):181–196, 1993.

    Google Scholar 

  16. K. Marriott, H. Søndergaard and N.D. Jones. Denotational abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems, ACM-TOPLAS, 16(3):607–648, 1994.

    Google Scholar 

  17. C. Mellish. Some Global Optimizations for a Prolog Compiler. The Journal of Logic Programming, 2(1):43–66, 1985.

    Google Scholar 

  18. H. Søndergaard. An Application of Abstract Interpretation of Logic Programs: Occur Check Reduction. Proc. ESOP '86, eds. B. Robinet and R. Wilhelm, Springer Verlag, pp. 327–338, LNCS 213, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, P.O. Box 94079, 1090, GB Amsterdam, The Netherlands

    Elena Marchiori

  2. University of Leiden, P.O. Box 9512, 2300, RA Leiden, The Netherlands

    Elena Marchiori

Authors
  1. Elena Marchiori
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Hanus Mario Rodríguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Marchiori, E. (1996). Prime factorizations of abstract domains using first-order logic. In: Hanus, M., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1996. Lecture Notes in Computer Science, vol 1139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61735-3_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-61735-3_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61735-8

  • Online ISBN: 978-3-540-70672-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation