Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Abstract Verification and Debugging of Constraint Logic Programs

  • Conference paper
  • First Online:
Recent Advances in Constraints (CologNet 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2627))

Abstract

The technique of Abstract Interpretation [13] has allowed the development of sophisticated program analyses which are provably correct and practical. The semantic approximations produced by such analyses have been traditionally applied to optimization during program compilation. However, recently, novel and promising applications of semantic approximations have been proposed in the more general context of program verification and debugging [3],[10],[7].

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.

Similar content being viewed by others

References

  1. K. R. Apt and E. Marchiori. Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing, 6(6):743–765, 1994.

    Article  MATH  Google Scholar 

  2. K. R. Apt and D. Pedreschi. Reasoning about termination of pure PROLOG programs. Information and Computation, 1(106):109–157, 1993.

    Article  MathSciNet  Google Scholar 

  3. F. Bourdoncle. Abstract debugging of higher-order imperative languages. In Programming Languages Design and Implementation’93, pages 46–55, 1993.

    Google Scholar 

  4. J. Boye, W. Drabent, and J. Małuszyński. Declarative diagnosis of constraint programs: an assertion-based approach. In Proc. of the 3rd. Int’l Workshop on Automated Debugging-AADEBUG’97, 123–141, Linköping, Sweden, May 1997. U. of Linköping Press.

    Google Scholar 

  5. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García, and G. Puebla. The Ciao Prolog System. Reference Manual. The Ciao System Documentation Series-TR CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), August 1997. System and on-line version of the manual available at http://clip.dia.fi.upm.es/Software/Ciao/.

  6. F. Bueno, D. Cabeza, M. Hermenegildo, and G. Puebla. Global Analysis of Standard Prolog Programs. In European Symposium on Programming, number 1058 in LNCS, pages 108–124, Sweden, April 1996. Springer-Verlag.

    Google Scholar 

  7. F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. Hermenegildo, J. Maluszynski, and G. Puebla. On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In Proc. of the 3rd. Int’l Workshop on Automated Debugging-AADEBUG’97, pages 155–170, Linköping, Sweden, May 1997. U. of Linköping Press.

    Google Scholar 

  8. D. Cabeza and M. Hermenegildo. The Ciao Module System: A New Module System for Prolog. In Special Issue on Parallelism and Implementation of (C)LP Systems, volume 30 of Electronic Notes in Theoretical Computer Science. Elsevier-North Holland, March 2000.

    Google Scholar 

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

    Article  Google Scholar 

  10. M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Proving properties of logic programs by abstract diagnosis. In M. Dams, editor, Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science, pages 22–50. Springer-Verlag, 1996.

    Google Scholar 

  11. M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Abstract diagnosis. Journal of Logic Programming, 39(1–3):43–93, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  12. M. Comini, G. Levi, and G. Vitiello. Declarative diagnosis revisited. In 1995 International Logic Programming Symposium, pages 275–287, Portland, Oregon, December 1995. MIT Press, Cambridge, MA.

    Google Scholar 

  13. P. Cousot and R. Cousot. Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

    Google Scholar 

  14. P.W. Dart and J. Zobel. A Regular Type Language for Logic Programs. In F. Pfenning, editor, Types in Logic Programming, pages 157–187. MIT Press, 1992.

    Google Scholar 

  15. P. Deransart. Proof methods of declarative properties of definite programs. Theoretical Computer Science, 118:99–166, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  16. P. Deransart, M. Hermenegildo, and J. Maluszynski. Analysis and Visualization Tools for Constraint Programming. Number 1870 in LNCS. Springer-Verlag, September 2000.

    Google Scholar 

  17. W. Drabent, S. Nadjm-Tehrani, and J. Małuszyński. The Use of Assertions in Algorithmic Debugging. In Proceedings of the Intl. Conf. on Fifth Generation Computer Systems, pages 573–581, 1988.

    Google Scholar 

  18. W. Drabent, S. Nadjm-Tehrani, and J. Maluszynski. Algorithmic debugging with assertions. In H. Abramson and M.H. Rogers, editors, Meta-programming in Logic Programming, pages 501–522. MIT Press, 1989.

    Google Scholar 

  19. G. Ferrand. Error diagnosis in logic programming. J. Logic Programming, 4:177–198, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  20. J. Gallagher and G. Puebla. Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs. In Fourth International Symposium on Practical Aspects of Declarative Languages, number 2257 in LNCS, pages 243–261. Springer-Verlag, January 2002.

    Chapter  Google Scholar 

  21. J.P. Gallagher and D.A. de Waal. Fast and precise regular approximations of logic programs. In Pascal Van Hentenryck, editor, Proc. of the 11th International Conference on Logic Programming, pages 599–613. MIT Press, 1994.

    Google Scholar 

  22. M. García de la Banda, M. Hermenegildo, M. Bruynooghe, V. Dumortier, G. Janssens, and W. Simoens. Global Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems, 18(5):564–615, September 1996.

    Article  Google Scholar 

  23. M. Hermenegildo. A Documentation Generator for (C)LP Systems. In International Conference on Computational Logic, CL2000, number 1861 in LNAI, pages 1345–1361. Springer-Verlag, July 2000.

    Google Scholar 

  24. M. Hermenegildo, F. Bueno, G. Puebla, and P. López-García. Program Analysis, Debugging and Optimization Using the Ciao System Preprocessor. In 1999 International Conference on Logic Programming, pages 52–66, Cambridge, MA, November 1999. MIT Press.

    Google Scholar 

  25. M. Hermenegildo, G. Puebla, and F. Bueno. Using Global Analysis, Partial Specifications, and an Extensible Assertion Language for Program Validation and Debugging. In K. R. Apt, V. Marek, M. Truszczynski, and D. S. Warren, editors, The Logic Programming Paradigm: a 25-Year Perspective, pages 161–192. Springer-Verlag, July 1999.

    Google Scholar 

  26. P. Hill and J. Lloyd. The Goedel Programming Language. MIT Press, Cambridge MA, 1994.

    MATH  Google Scholar 

  27. Y. Lichtenstein and E. Y. Shapiro. Abstract algorithmic debugging. In R. A. Kowalski and K. A. Bowen, editors, Fifth International Conference and Symposium on Logic Programming, pages 512–531, Seattle, Washington, August 1988. MIT.

    Google Scholar 

  28. K. Muthukumar and M. Hermenegildo. Compile-time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming, 13(2/3):315–347, July 1992.

    Article  MATH  Google Scholar 

  29. G. Puebla, F. Bueno, and M. Hermenegildo. A Generic Preprocessor for Program Validation and Debugging. In P. Deransart, M. Hermenegildo, and J. Maluszynski, editors, Analysis and Visualization Tools for Constraint Programming, number 1870 in LNCS, pages 63–107. Springer-Verlag, September 2000.

    Chapter  Google Scholar 

  30. G. Puebla, F. Bueno, and M. Hermenegildo. An Assertion Language for Constraint Logic Programs. In P. Deransart, M. Hermenegildo, and J. Maluszynski, editors, Analysis and Visualization Tools for Constraint Programming, number 1870 in LNCS, pages 23–61. Springer-Verlag, September 2000.

    Chapter  Google Scholar 

  31. G. Puebla, F. Bueno, and M. Hermenegildo. Combined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs. In Logic-based Program Synthesis and Transformation (LOPSTR’99), number 1817 in LNCS, pages 273–292. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  32. Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury: an efficient purely declarative logic programming language. JLP, 29(1–3), October 1996.

    Google Scholar 

  33. C. Vaucheret and F. Bueno. More precise yet efficient type inference for logic programs. In International Static Analysis Symposium, number 2477 in LNCS, pages 102–116. Springer-Verlag, September 2002.

    Google Scholar 

  34. E. Vetillard. Utilisation de Declarations en Programmation Logique avec Constraintes. PhD thesis, U. of Aix-Marseilles II, 1994.

    Google Scholar 

  35. E. Yardeni and E. Shapiro. A Type System for Logic Programs. Concurrent Prolog: Collected Papers, pages 211–244, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technical University of Madrid (UPM), Spain

    Manuel Hermenegildo, Germán Puebla, Francisco Bueno & Pedro López-García

Authors
  1. Manuel Hermenegildo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Germán Puebla
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Francisco Bueno
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pedro López-García
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University College Cork, Ireland

    Barry O’Sullivan

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hermenegildo, M., Puebla, G., Bueno, F., López-García, P. (2003). Abstract Verification and Debugging of Constraint Logic Programs. In: O’Sullivan, B. (eds) Recent Advances in Constraints. CologNet 2002. Lecture Notes in Computer Science, vol 2627. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36607-5_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-36607-5_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00986-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation