Skip to main content
SpringerLink
Log in

Forward versus Backward Verification of Logic Programs

  • Conference paper
Book cover Logic Programming (ICLP 2003)

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

Included in the following conference series:

Abstract

One recent development in logic programming has been the application of abstract interpretation to verify the partial correctness of a logic program with respect to a given set of assertions. One approach to verification is to apply forward analysis that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify that the assertions hold. The dual approach is to apply backward analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. This paper is a systematic comparison of these two approaches to verification. The paper reports some equivalence results that relate the relative power of various forward and backward analysis frameworks.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 99.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aiken, A., Lakshman, T.K.: Directional Type Checking of Logic Programs. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 43–60. Springer, Heidelberg (1994)

    Google Scholar 

  2. Birkhoff, G.: Lattice Theory. AMS Press (1967)

    Google Scholar 

  3. Bruynooghe, M.: A Practical Framework for the Abstract Interpretation of Logic Programs. The Journal of Logic Programming 10(1,2,3,4), 91–124 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  4. Codish, M., Lagoon, V.: Type Dependencies for Logic Programs using ACIunification. Theoretical Computer Science 238, 131–159 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Codish, M., Taboch, C.: A Semantic Basis for the Termination Analysis of Logic Programs. The Journal of Logic Programming 41(1), 103–123 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  6. Comini, M., Gori, R., Levi, G., Volpe, P.: Abstract Interpretation based Verification of Logic Programs. Electronic Notes of Theoretical Computer Science, vol. 30(1) (1999)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract Interpretation and Application to Logic Programs. The Journal of Logic Programming 13(2-3), 103–179 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  8. Drabent, W., Maluszyński, J.: Inductive Assertion Method for Logic Programs. Theoretical Computer Science 59(1), 133–155 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  9. Duesterwald, E., Gupta, R., Soffa, M.L.: Demand-driven Computation of Interprocedural Data Flow. In: Principles of Programming Languages, pp. 37–48. ACM, New York (1995)

    Google Scholar 

  10. Fecht, C., Seidl, H.: A Faster Solver for General Systems of Equations. Science of Computer Programming 35(2-3), 137–162 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  11. García de la Banda, M., Marriott, K., Stuckey, P.J., Søndergaard, H.: Differential Methods in Logic Program Analysis. The Journal of Logic Programming 35(1), 1–37 (1998)

    Article  MATH  Google Scholar 

  12. Genaim, S., Codish, M.: Inferring Termination Conditions for Logic Programs using Backwards Analysis. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 681–690. Springer, Heidelberg (2001); Technical report version available at http://www.cs.bgu.ac.il/~mcodish/Papers/Pages/lpar01.html

    Chapter  Google Scholar 

  13. Giacobazzi, R., Scozzari, F.: A Logical Model for Relational Abstract Domains. ACM Transactions on Programming Languages and Systems 20(5), 1067–1109 (1998)

    Article  Google Scholar 

  14. Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.: Incremental analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 22(2), 187–223 (2000)

    Article  Google Scholar 

  15. Hughes, R.J.M., Launchbury, J.: Reversing Abstract Interpretations. Science of Computer Programming 22(3), 307–326 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Jacobs, D., Langen, A.: Static Analysis of Logic Programs for Independent And-Parallelism. The Journal of Logic Programming 13(1/2/3&4), 291–314 (1992)

    Article  MATH  Google Scholar 

  17. King, A., Lu, L.: A Backward Analysis for Constraint Logic Programs. Theory and Practice of Logic Programming 2(4-5), 517–547 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  18. King, A., Lu, L.: Forward versus Backward Verification of Logic Programs. Technical Report 5-03, Computing Laboratory, University of Kent (April 2003)

    Google Scholar 

  19. Langen, A.: Advanced Techniques for Approximating Variable Aliasing in Logic Programs. PhD thesis, Computer Science Department, University of Southern California, Los Angeles (1991)

    Google Scholar 

  20. Le Charlier, B., Leclére, C., Rossi, S., Cortesi, A.: Automatic Verification of Prolog Programs. The Journal of Logic Programming 39(1-3), 3–42 (1999)

    Article  MATH  Google Scholar 

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

    Article  Google Scholar 

  22. Lindenstrauss, N., Sagiv, Y.: Automatic Termination Analysis of Logic Programs. In: International Conference on Logic Programming, pp. 63–77. MIT Press, Cambridge (1997)

    Google Scholar 

  23. Lu, L., King, A.: Backward Type Inference Generalises Type Checking. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 85–101. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Mesnard, F., Ruggieri, S.: On Proving Left Termination of Constraint Logic Programs. ACM Transactions on Computational Logic 4(2), 207–259 (2003)

    Article  MathSciNet  Google Scholar 

  25. Miné, A.: The Octagon Abstract Domain. In: Eighth Working Conference on Reverse Engineering, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  26. Puebla, G., Bueno, F., Hermenegildo, M.: An Assertion Language for Constraint Logic Programs. In: Deransart, P., Małuszyński, J. (eds.) DiSCiPl 1999. LNCS, vol. 1870, pp. 23–61. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Schachte, P.: Precise and Efficient Static Analysis of Logic Programs. PhD thesis, Department of Computer Science, University of Melbourne (1999)

    Google Scholar 

  28. Schachte, P.: Precise Goal-independent Abstract Interpretation of Constraint Logic Programs. Theoretical Computer Science 293(3), 557–577 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  29. van Dalen, D.: Logic and Structure. Springer, Heidelberg (1997)

    Google Scholar 

  30. Volpe, P.: A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs. Science of Computer Programming 39(1), 125–148 (2001)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Kent, Canterbury, CT2 7NF, UK

    Andy King

  2. Department of Computer Science, Oakland University, Rochester, MI, 48309, USA

    Lunjin Lu

Authors
  1. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lunjin Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ecole Polytechnique, Rue de Saclay, 91128, Palaiseau Cedex, France

    Catuscia Palamidessi

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

King, A., Lu, L. (2003). Forward versus Backward Verification of Logic Programs. In: Palamidessi, C. (eds) Logic Programming. ICLP 2003. Lecture Notes in Computer Science, vol 2916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24599-5_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24599-5_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20642-2

  • Online ISBN: 978-3-540-24599-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation