Skip to main content
SpringerLink
Log in
Book cover

Annual Asian Computing Science Conference

ASIAN 1997: Advances in Computing Science — ASIAN'97 pp 225–238Cite as

Automated verification of behavioural properties of prolog programs

  • Session 5
  • Conference paper
  • First Online:

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

Abstract

Program verification is a crucial issue in the field of program development, compilation and debugging. In this paper, we present an analyser for Prolog which aims at verifying whether the execution of a program behaves according to a given specification (behavioural assumptions). The analyser is based on the methodology of abstract interpretation. A novel notion of abstract sequence is introduced, that includes an over- approximatimation of successful inputs (this is useful to detect mutual exclusion of clauses, and expresses size relation information between successful inputs and the corresponding outputs, together with cardinality information in terms of input argument sizes.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.

    Google Scholar 

  2. C. Braem, B. Le Charlier, S. Modard, and P. Van Hentenryck. Cardinality Analysis of Prolog. In M. Bruynooghe, editor, Proc. of the International Logic Programming Symposium (ILPS'94), Ithaca NY, USA, November 1994. MIT Press.

    Google Scholar 

  3. A. Cortesi, B. Le Charlier, and S. Rossi. Specification-Based Automatic Verification of Logic Programs. In Logic Program Synthesis and Transformation. Proceedings of the 6th International Workshop, LOPSTR'96, volume 1207 of LNCS. Springer Verlag, August 1996.

    Google Scholar 

  4. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combination of Abstract Domains for Logic Programming. In Proc. of the 21th ACM Symposium on Principles of Programming Languages (POPL'94), Portland, Oregon, January 1994.

    Google Scholar 

  5. P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

    Google Scholar 

  6. P. De Boeck and B. Le Charlier. Static Type Analysis of Prolog Procedures for Ensuring Correctness. In PLILP'90, LNCS 456, Springer-Verlag, pages 222–237, Linköping, Sweden, 1990.

    Google Scholar 

  7. Y. Deville. Logic Programming: Systematic Program Development. MIT Press, 1990.

    Google Scholar 

  8. Thomas W. Getzinger. The Costs and Benefits of Abstract Interpretation-driven Prolog Optimization. In SAS'94, LNCS 864, Springer-Verlag, pages 1–25, 1994.

    Google Scholar 

  9. J. Henrard and B. Le Charlier. FOLON: An Environment for Declarative Construction of Logic Programs. In M. Bruynooghe and M. Wirsing, editors, PLILP'92, LNCS 631, Springer-Verlag, Leuven, 1992.

    Google Scholar 

  10. B. Le Charlier, C. Leclère, S. Rossi, and A. Cortesi. Automated Verification of Prolog Programs. Technical Report RP-97-003, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique, March 1997.

    Google Scholar 

  11. B. Le Charlier and S. Rossi. Sequence-Based Abstract Semantics of Prolog. Technical Report RR-96-001, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique, February 1996.

    Google Scholar 

  12. B. Le Charlier, S. Rossi, and P. Van Hentenryck. An Abstract Interpretation Framework Which Accurately Handles Prolog Search-Rule and the Cut. In M. Bruynooghe, editor, ILPS'94, Ithaca NY, USA, November 1994. MIT Press.

    Google Scholar 

  13. B. Le Charlier, S. Rossi, and P. Van Hentenryck. Sequence-Based Abstract Interpretation of Prolog. Technical Report RR-97-001, Facultés Universitaires Notre-Dame de la Paix, Institut d'Informatique, January 1997.

    Google Scholar 

  14. B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(1):35–101, January 1994.

    Article  Google Scholar 

  15. B. Le Charlier and P. Van Hentenryck. Reexecution in Abstract Interpretation of Prolog. Acta Informatica, 32:209–253, 1995.

    Article  Google Scholar 

  16. C. Leclère and B. Le Charlier. Two Dual Abstract Operations to Duplicate, Eliminate, Equalize, Introduce and Rename Place-Holders Occurring Inside Abstract Descriptions. Technical Report RP-96-028, University of Namur, Belgium, 1996.

    Google Scholar 

  17. J.W. Lloyd. Foundations of Logic Programming. Springer Series: Symbolic Computation-Artificial Intelligence. Springer-Verlag, second edition, 1987.

    Google Scholar 

  18. P. Van Roy. 1983-1993: The Wonder Years of Sequential Prolog Implementation. Journal of Logic Programming, 19/20:385–441, 1994.

    Article  Google Scholar 

  19. D. K. Wilde. A Library for Doing Polyhedral Operations. Technical Report No. 785, IRISA, Rennes Cedex-France, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut d'Informatique, 21 rue Grandgagnage, B-5000, Namur, Belgium

    B. Le Charlier & C. Leclère

  2. Dip. di Matematica, via Belzoni 7, 35131, Padova, Ital

    S. Rossi

  3. Dip. di Matematica e Informatica, via Torino 155, 30173, Venezia, Italy

    A. Cortesi

Authors
  1. B. Le Charlier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C. Leclère
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. S. Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. Cortesi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

R. K. Shyamasundar K. Ueda

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Le Charlier, B., Leclère, C., Rossi, S., Cortesi, A. (1997). Automated verification of behavioural properties of prolog programs. In: Shyamasundar, R.K., Ueda, K. (eds) Advances in Computing Science — ASIAN'97. ASIAN 1997. Lecture Notes in Computer Science, vol 1345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63875-X_55

Download citation

  • DOI: https://doi.org/10.1007/3-540-63875-X_55

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63875-9

  • Online ISBN: 978-3-540-69658-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation