Automated verification of behavioural properties of prolog programs

  • B. Le Charlier
  • C. Leclère
  • S. Rossi
  • A. Cortesi
Session 5
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


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.


Program Verification Static Analysis Logic Programming Prolog 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K.R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.Google Scholar
  2. 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. 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. 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. 5.
    P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.Google Scholar
  6. 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. 7.
    Y. Deville. Logic Programming: Systematic Program Development. MIT Press, 1990.Google Scholar
  8. 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. 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. 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. 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. 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. 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. 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.CrossRefGoogle Scholar
  15. 15.
    B. Le Charlier and P. Van Hentenryck. Reexecution in Abstract Interpretation of Prolog. Acta Informatica, 32:209–253, 1995.CrossRefGoogle Scholar
  16. 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. 17.
    J.W. Lloyd. Foundations of Logic Programming. Springer Series: Symbolic Computation-Artificial Intelligence. Springer-Verlag, second edition, 1987.Google Scholar
  18. 18.
    P. Van Roy. 1983-1993: The Wonder Years of Sequential Prolog Implementation. Journal of Logic Programming, 19/20:385–441, 1994.CrossRefGoogle Scholar
  19. 19.
    D. K. Wilde. A Library for Doing Polyhedral Operations. Technical Report No. 785, IRISA, Rennes Cedex-France, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • B. Le Charlier
    • 1
  • C. Leclère
    • 1
  • S. Rossi
    • 2
  • A. Cortesi
    • 3
  1. 1.Institut d'InformatiqueNamurBelgium
  2. 2.Dip. di MatematicaPadovaItal
  3. 3.Dip. di Matematica e InformaticaVeneziaItaly

Personalised recommendations