Skip to main content
SpringerLink
Log in

Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming

  • Chapter
A 25-Year Perspective on Logic Programming

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6125))

Abstract

We survey some general principles and methodologies for program analysis and verification. In particular, we focus on abstract interpretation and model checking techniques, and on their applications to constraint logic programs.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.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. Andreoli, J.-M., Pareschi, R.: Linear Ojects. Logical Processes with Built-in Inheritance. New Generation Comput. 9(3/4), 445–474 (1991)

    Article  Google Scholar 

  2. Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391–397. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Bagnara, R., Hill, P., Zaffanella, E.: Set-sharing is redundant for pair-sharing. Theor. Comput. Sci. 277(1-2), 3–46 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bozzano, M., Delzanno, G., Martelli, M.: Model Checking Linear Logic Specifications. TPLP 4(5-6), 573–619 (2004)

    MATH  MathSciNet  Google Scholar 

  5. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comp. Sci. 59, 115–131 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  6. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. In: Proc. IEEE LICS 1990, pp. 428–439 (1990)

    Google Scholar 

  7. Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. ENTCS 40 (2000)

    Google Scholar 

  8. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 176–194. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  10. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  11. Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., Ranzato, F.: Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst. 19(1), 7–47 (1997)

    Article  Google Scholar 

  12. Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program. 38(1-3), 27–71 (2000)

    Article  MATH  Google Scholar 

  13. Cousot, P.: Types as abstract interpretations (invited paper). In: Proc. ACM POPL 1997, pp. 316–331 (1997)

    Google Scholar 

  14. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1-2), 47–103 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  15. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL  1977), pp. 238–252. ACM Press, New York (1977)

    Google Scholar 

  16. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press, New York (1979)

    Google Scholar 

  17. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2-3), 103–179 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  18. Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) (invited paper). In: Proc. of the 1994 IEEE Internat. Conf. on Computer Languages (ICCL 1994), pp. 95–112 (1994)

    Google Scholar 

  19. Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27th ACM POPL, pp. 12–25 (2000)

    Google Scholar 

  20. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)

    Google Scholar 

  21. Cousot, P., Cousot, R., Giacobazzi, R.: Abstract interpretation of resolution-based semantics. Theor. Comput. Sci. 410(46), 4724–4746 (2009)

    Article  MATH  Google Scholar 

  22. Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1997)

    Google Scholar 

  23. Delzanno, G.: An Overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. ENTCS 76 (2002)

    Google Scholar 

  24. Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. Dong, Y., Du, X., Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Sokolsky, O., Stark, E.W., Scott Warren, D.: Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 74–88. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  26. Falaschi, M., Levi, G., Palamidessi, C., Martelli, M.: Declarative modeling of the operational behavior of logic languages. Theor. Comput. Sci. 69(3), 289–318 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  27. Filé, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv. 28(2), 333–336 (1996)

    Article  Google Scholar 

  28. Filé, G., Ranzato, F.: Complementation of abstract domains made easy. In: Proc. of the 1996 Joint Internat. Conf. and Symp. on Logic Programming (JICSLP 1996), pp. 348–362 (1996)

    Google Scholar 

  29. Fioravanti, F., Pettorossi, A., Proietti, M.: Verification of Sets of Infinite State Processes Using Program Transformation. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 111–128. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Fribourg, L., Richardson, J.: Symbolic Verification with Gap-Order Constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 20–37. Springer, Heidelberg (1997)

    Google Scholar 

  31. Fribourg, L., Olsén, H.: A Decompositional Approach for Computing Least Fixed-Points of Datalog Programs with Z-Counters. Constraints 2(3/4), 305–335 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  32. Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Automated Reasoning 31(1), 73–103 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  33. Giacobazzi, R., Mastroeni, I.: Compositionality in the puzzle of semantics. In: Proc. of the ACM Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2002), pp. 87–97 (2002)

    Google Scholar 

  34. Giacobazzi, R., Mastroeni, I.: Transforming semantics by abstract interpretation. Theor. Comput. Sci. 337(1-3), 1–50 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  35. Giacobazzi, R., Mastroeni, I.: Transforming abstract interpretations by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 1–17. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  36. Giacobazzi, R., Palamidessi, C., Ranzato, F.: Weak relative pseudo-complements of closure operators. Algebra Universalis 36(3), 405–412 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  37. Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  38. Giacobazzi, R., Ranzato, F.: Complementing logic program semantics. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 238–253. Springer, Heidelberg (1996)

    Google Scholar 

  39. Giacobazzi, R., Ranzato, F.: Refining and compressing abstract domains. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 771–781. Springer, Heidelberg (1997)

    Google Scholar 

  40. Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program 32(1-3), 177–210 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  41. Giacobazzi, R., Ranzato, F.: Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Information and Computation 145(2), 153–190 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  42. Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci 216, 159–211 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  43. Giacobazzi, R., Ranzato, F.: Incompleteness of states w.r.t. traces in model checking. Information and Computation 204(3), 376–407 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  44. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  45. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract domains condensing. ACM Transactions on Computational Logic 6(1), 33–60 (2005)

    Article  MathSciNet  Google Scholar 

  46. Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (1998)

    Article  Google Scholar 

  47. van Glabbeek, R.J., Ploeger, B.: Correcting a space-efficient simulation algorithm. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 517–529. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  48. Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  49. Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: Proc. IEEE Real-Time Systems Symposium 1997, pp. 230–239 (1997)

    Google Scholar 

  50. Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462 (1995)

    Google Scholar 

  51. Henzinger, T.A., Maujumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Comput. Log. 6(1), 1–31 (2005)

    Article  MathSciNet  Google Scholar 

  52. Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst. 19(5), 751–803 (1997)

    Article  Google Scholar 

  53. Leuschel, M., Lehmann, H.: Coverability of reset petri nets and other well-structured transition systems by partial deduction. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 101–115. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  54. Leuschel, M., Lehmann, H.: Solving coverability problems of petri nets by partial deduction. In: Proc. PPDP 2000, pp. 268–279 (2000)

    Google Scholar 

  55. Leuschel, M., Massart, T.: Infinite State Model Checking by Abstract Interpretation and Program Specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 62–81. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  56. Levi, G., Spoto, F.: An experiment in domain refinement: Type domains and type representations for logic programs. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 152–169. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  57. Levi, G., Spoto, F.: Non pair-sharing and freeness analysis through linear refinement. In: Proc. ACM PEPM, pp. 52–61 (2000)

    Google Scholar 

  58. Levi, G., Spoto, F.: Pair-independence and freeness analysis through linear refinement. Information and Computation 182(1), 14–52 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  59. López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Proc. PPDP 2005, pp. 35–46 (2005)

    Google Scholar 

  60. Mycroft, A.: Completeness and predicate-based abstract interpretation. In: Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM 1993), pp. 179–185 (1993)

    Google Scholar 

  61. Nielson, F.: Expected forms of data flow analyses. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol. 217, pp. 172–191. Springer, Heidelberg (1986)

    Google Scholar 

  62. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 977–982 (1987)

    Article  MathSciNet  Google Scholar 

  63. Pettorossi, A., Proietti, M., Senni, V.: Transformational Verification of Parameterized Protocols Using Array Formulas. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol. 3901, pp. 23–43. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  64. Ramakrishnan, C.R.: A Model Checker for Value-Passing Mu-Calculus Using Logic Programming. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 1–13. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  65. Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient Model Checking Using Tabled Resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)

    Google Scholar 

  66. Ranzato, F., Tapparo, F.: A new efficient simulation equivalence algorithm. In: Proc. 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pp. 171–180 (2007)

    Google Scholar 

  67. Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation. Information and Computation 206(5), 620–651 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  68. Rosenthal, K.I.: Quantales and their applications. In: Pitman Research Notes in Mathematics. Longman Scientific & Technical, London (1990)

    Google Scholar 

  69. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of Parameterized Systems Using Logic Program Transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  70. Roychoudhury, A., Ramakrishnan, C.R.: Unfold/Fold Transformations for Automated Verification of Parameterized Concurrent Systems. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 261–290. Springer, Heidelberg (2004)

    Google Scholar 

  71. Scozzari, F.: Logical optimality of groundness analysis. Theor. Comput. Sci. 277(1-2), 149–184 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  72. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-Based Model Checking of Ad Hoc Network Protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 603–619. Springer, Heidelberg (2009)

    Google Scholar 

  73. Spoto, F.: Optimality and condensing of information flow through linear refinement. Theor. Comput. Sci. 388(1-3), 53–82 (2007)

    MATH  MathSciNet  Google Scholar 

  74. Strachey, C.: The varieties of programming language. In: Proc. of the International Computing Symposium, Cini Foundation, Venice, pp. 222–233. Springer, Heidelberg (1972)

    Google Scholar 

  75. Tan, L., Cleaveland, W.R.: Simulation revisited. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 480–495. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  76. Urbina, L.: Analysis of Hybrid Systems in CLP(R). In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 451–467. Springer, Heidelberg (1996)

    Google Scholar 

  77. Yang, P., Basu, S., Ramakrishnan, C.R.: Parameterized Verification of π-Calculus Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 42–57. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università di Genova, Italy

    Giorgio Delzanno

  2. Università di Verona, Italy

    Roberto Giacobazzi

  3. Università di Padova, Italy

    Francesco Ranzato

Authors
  1. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roberto Giacobazzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Francesco Ranzato
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dip. di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100, Udine, Italy

    Agostino Dovier

  2. Department of Computer Science, New Mexico State University, P.O. Box 30001, 88003, MSC CS, Las Cruces, NM, USA

    Enrico Pontelli

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Delzanno, G., Giacobazzi, R., Ranzato, F. (2010). Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming. In: Dovier, A., Pontelli, E. (eds) A 25-Year Perspective on Logic Programming. Lecture Notes in Computer Science, vol 6125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14309-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14309-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14308-3

  • Online ISBN: 978-3-642-14309-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation