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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andreoli, J.-M., Pareschi, R.: Linear Ojects. Logical Processes with Built-in Inheritance. New Generation Comput. 9(3/4), 445–474 (1991)
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)
Bagnara, R., Hill, P., Zaffanella, E.: Set-sharing is redundant for pair-sharing. Theor. Comput. Sci. 277(1-2), 3–46 (2002)
Bozzano, M., Delzanno, G., Martelli, M.: Model Checking Linear Logic Specifications. TPLP 4(5-6), 573–619 (2004)
Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comp. Sci. 59, 115–131 (1988)
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)
Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. ENTCS 40 (2000)
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)
Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., Ranzato, F.: Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst. 19(1), 7–47 (1997)
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)
Cousot, P.: Types as abstract interpretations (invited paper). In: Proc. ACM POPL 1997, pp. 316–331 (1997)
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)
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)
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)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2-3), 103–179 (1992)
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)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27th ACM POPL, pp. 12–25 (2000)
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)
Cousot, P., Cousot, R., Giacobazzi, R.: Abstract interpretation of resolution-based semantics. Theor. Comput. Sci. 410(46), 4724–4746 (2009)
Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1997)
Delzanno, G.: An Overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. ENTCS 76 (2002)
Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)
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)
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)
Filé, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv. 28(2), 333–336 (1996)
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)
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)
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)
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)
Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Automated Reasoning 31(1), 73–103 (2003)
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)
Giacobazzi, R., Mastroeni, I.: Transforming semantics by abstract interpretation. Theor. Comput. Sci. 337(1-3), 1–50 (2005)
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)
Giacobazzi, R., Palamidessi, C., Ranzato, F.: Weak relative pseudo-complements of closure operators. Algebra Universalis 36(3), 405–412 (1996)
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)
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)
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)
Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program 32(1-3), 177–210 (1998)
Giacobazzi, R., Ranzato, F.: Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Information and Computation 145(2), 153–190 (1998)
Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci 216, 159–211 (1999)
Giacobazzi, R., Ranzato, F.: Incompleteness of states w.r.t. traces in model checking. Information and Computation 204(3), 376–407 (2006)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract domains condensing. ACM Transactions on Computational Logic 6(1), 33–60 (2005)
Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (1998)
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)
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)
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)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462 (1995)
Henzinger, T.A., Maujumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Comput. Log. 6(1), 1–31 (2005)
Jensen, T.P.: Disjunctive program analysis for algebraic data types. ACM Trans. Program. Lang. Syst. 19(5), 751–803 (1997)
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)
Leuschel, M., Lehmann, H.: Solving coverability problems of petri nets by partial deduction. In: Proc. PPDP 2000, pp. 268–279 (2000)
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)
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)
Levi, G., Spoto, F.: Non pair-sharing and freeness analysis through linear refinement. In: Proc. ACM PEPM, pp. 52–61 (2000)
Levi, G., Spoto, F.: Pair-independence and freeness analysis through linear refinement. Information and Computation 182(1), 14–52 (2003)
López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Proc. PPDP 2005, pp. 35–46 (2005)
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)
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)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 977–982 (1987)
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)
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)
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)
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)
Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation. Information and Computation 206(5), 620–651 (2008)
Rosenthal, K.I.: Quantales and their applications. In: Pitman Research Notes in Mathematics. Longman Scientific & Technical, London (1990)
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)
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)
Scozzari, F.: Logical optimality of groundness analysis. Theor. Comput. Sci. 277(1-2), 149–184 (2002)
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)
Spoto, F.: Optimality and condensing of information flow through linear refinement. Theor. Comput. Sci. 388(1-3), 53–82 (2007)
Strachey, C.: The varieties of programming language. In: Proc. of the International Computing Symposium, Cini Foundation, Venice, pp. 222–233. Springer, Heidelberg (1972)
Tan, L., Cleaveland, W.R.: Simulation revisited. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 480–495. Springer, Heidelberg (2001)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)