Narrowing and rewriting logic: from foundations to applications.

*(English)*Zbl 1279.68205
López Fraguas, Francisco J. (ed.), Proceedings of the 15th workshop on functional and (constraint) logic programming (WFLP 2006), Madrid, Spain, November 16–17, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 177, 5-33 (2007).

Summary: Narrowing was originally introduced to solve equational \(E\)-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both cases, narrowing supports equational reasoning and assumes confluent equations. The main goal of this work is to show that narrowing can be greatly generalized, so as to support a much wider range of applications, when it is performed with rewrite theories \((\Sigma, E, R)\), where \((\Sigma, E)\) is an equational theory, and \(R\) is a collection of rewrite rules with no restrictions. Such theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo \(E\), and whose transitions are specified by \(R\). In this context, narrowing is generalized from an equational reasoning technique to a symbolic model checking technique for reachability analysis of a, typically infinite, concurrent system. We survey the foundations of this approach, suitable narrowing strategies, and various applications to security protocol verification, theorem proving, and programming languages.

For the entire collection see [Zbl 1275.68023].

For the entire collection see [Zbl 1275.68023].

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

03B70 | Logic in computer science |

68Q42 | Grammars and rewriting systems |

PDF
BibTeX
XML
Cite

\textit{S. Escobar} et al., Electron. Notes Theor. Comput. Sci. 177, 5--33 (2007; Zbl 1279.68205)

Full Text:
DOI

##### References:

[1] | Albert, E.; Vidal, G., The narrowing-driven approach to functional logic program specialization, New generation computing, 20, 1, 3-26, (2001) · Zbl 1016.68024 |

[2] | Alpuente, M.; Falaschi, M.; Vidal, G., Partial evaluation of functional logic programs, AC transactions on programming languages and systems, 20, 768-844, (1998) |

[3] | Alpuente, M.; Lucas, S.; Hanus, M.; Vidal, G., Specialization of functional logic programs based on needed narrowing, Theory and practice of logic programming, 5, 273-303, (2005) · Zbl 1092.68018 |

[4] | Antoy, S., Definitional trees, (), 143-157 |

[5] | Antoy, S., R. Echahed and M. Hanus, Parallel evaluation strategies for functional logic languages, in: Proc. of the Fourteenth International Conference on Logic Programming (ICLP’97) (1997), pp. 138-152 |

[6] | Antoy, S.; Echahed, R.; Hanus, M., A needed narrowing strategy, Journal of the ACM, 47, 4, 776-822, (2000) · Zbl 1327.68141 |

[7] | Bouajjani, A.; Mayr, R., Model checking lossy vector addition systems, (), 323-333 · Zbl 0926.03035 |

[8] | Bouhoula, A.; Rusinowitch, M., Implicit induction in conditional theories, Journal of automated reasoning, 14, 189-235, (1995) · Zbl 0819.68114 |

[9] | Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification over infinite states, (), 545-623 · Zbl 1035.68067 |

[10] | Clarke, E.M.; Grumberg, O.; Long, D.E., Model checking and abstraction, ACM transactions on programming languages and systems, 16, 1512-1542, (1994) |

[11] | Clavel, M.; Durán, F.; Eker, S.; Meseguer, J., Building equational proving tools by reflection in rewriting logic, (), 1-31 |

[12] | Comon, H.; Nieuwenhuis, R., Induction = I-axiomatization + first-order consistency, Information and computation, 159, 151-186, (2000) · Zbl 1046.68640 |

[13] | De Schreye, D.; Glück, R.; Jørgensen, J.; Leuschel, M.; Martens, B.; Sørensen, M., Conjunctive partial deduction: foundations, control, algorithms, and experiments, Journal of logic programming, 41, 231-277, (1999) · Zbl 0944.68025 |

[14] | Denker, G., J. Meseguer and C.L. Talcott, Protocol specification and analysis in Maude, in: N. Heintze and J. Wing, editors, Proceedings of Workshop on Formal Methods and Security Protocols, June 25, 1998, Indianapolis, Indiana, 1998, http://www.cs.bell-labs.com/who/nch/fmsp/index.html |

[15] | Dershowitz, N., S. Mitra and G. Sivakumar, Decidable matching for convergent systems (preliminary version)., in: D. Kapur, editor, 11th International Conference on Automated Deduction (CADE-11), Lecture Notes in Computer Science \bf607 (1992), pp. 589-602 |

[16] | Dolev, D.; Yao, A., On the security of public key protocols, IEEE transaction on information theory, 29, 198-208, (1983) · Zbl 0502.94005 |

[17] | Emerson, A. and K. Namjoshi, On model checking for nondeterministic infinite state systems, in: 13thIEEE Symposium on Logic in Computer Science, 1998, pp. 70-80 · Zbl 0945.68523 |

[18] | Escobar, S., Refining weakly outermost-needed rewriting and narrowing, in: D. Miller, editor, Proc. of 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’03 (2003), pp. 113-123 |

[19] | Escobar, S., Implementing natural rewriting and narrowing efficiently, (), 147-162 · Zbl 1122.68371 |

[20] | Escobar, S., C. Meadows and J. Meseguer, A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties, Theoretical Computer Science \bf367(1-2), pp. 162-202 · Zbl 1153.94375 |

[21] | Escobar, S.; Meseguer, J.; Thati, P., Natural narrowing for general term rewriting systems, (), 279-293 · Zbl 1078.68655 |

[22] | Fabrega, F.J.T.; Herzog, J.C.; Guttman, J., Strand spaces: proving security protocols correct, Journal of computer security, 7, 191-230, (1999) |

[23] | Fay, M., First order unification in equational theories, (), 161-167 |

[24] | Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoretical computer science, 256, 63-92, (2001) · Zbl 0973.68170 |

[25] | Genet, T. and V.V.T. Tong, Reachability analysis of term rewriting systems with Timbuk, in: 8thInternational Conference on Logic for Programming, Lecture Notes in Computer Science \bf2250, 2001 · Zbl 1275.68083 |

[26] | Goguen, J.; Meseguer, J., Equality, types, modules and (why not?) generics for logic programming, Journal of logic programming, 1, 179-210, (1984) · Zbl 0575.68091 |

[27] | Goguen, J.; Meseguer, J., Models and equality for logical programming, (), 1-22 |

[28] | Graf, S.; Saidi, H., Construction of abstract state graphs with PVS, (), 72-83 |

[29] | Hanus, M., The integration of functions into logic programming: from theory to practice, Journal of logic programming, 19&20, 583-628, (1994) · Zbl 0942.68526 |

[30] | Hanus, M., S. Antoy, H. Kuchen, F. López-Fraguas, W. Lux, J. Moreno Navarro and F. Steiner, Curry: An Integrated Functional Logic Language (version 0.8), Available at: http://www.informatik.uni-kiel.de/ curry (2003) |

[31] | Hudak, P., P.L. Wadeler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, K. Hammond, J. Hughes, T. Johnsson, R. Kieburtz, R.S. Nikhil, S.L. Peyton-Jones, M. Reeve, D. Wise and J. Young, Report on the functional programming language haskell, Technical report, Department of Computer Science, Glasgow University (1990) |

[32] | Huet, G.; Lévy, J.-J., Computations in orthogonal term rewriting systems, part I + II, (), 395-414, and 415-443 |

[33] | Hullot, J., Canonical forms and unification, (), 318-334 |

[34] | Jones, N.; Gomard, C.; Sestoft, P., Partial evaluation and automatic program generation, (1993), Prentice-Hall Englewood Cliffs, NJ · Zbl 0875.68290 |

[35] | Jouannaud, J.-P.; Kirchner, C.; Kirchner, H., Incremental construction of unification algorithms in equational theories, (), 361-373 |

[36] | Kesten, Y.; Pnueli, A., Control and data abstraction: the cornerstones of practical formal verification, International journal on software tools for technology transfer, 4, 328-342, (2000) · Zbl 1059.68589 |

[37] | Lafave, L.; Gallagher, J., Constraint-based partial evaluation of rewriting-based functional logic programs, (), 168-188 |

[38] | Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S., Property preserving abstractions for the verification of concurrent systems, Formal methods in system design, 6, 1-36, (1995) · Zbl 0829.68053 |

[39] | Lowe, G., Breaking and fixing the needham-schroeder public-key protocol using fdr, (), 147-166 |

[40] | Martí-Oliet, N.; Meseguer, J., Rewriting logic as a logical and semantic framework, (), 1-87, first published as SRI Tech. Report SRI-CSL-93-05, August 1993 |

[41] | Meadows, C., The NRL protocol analyzer: an overview, The journal of logic programming, 26, 113-131, (1996) · Zbl 0871.68052 |

[42] | Meseguer, J., General logics, in: H.-D. E. et al., editor, Logic Colloquium’87 (1989), pp. 275-329 · Zbl 0691.03001 |

[43] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical computer science, 96, 73-155, (1992) · Zbl 0758.68043 |

[44] | Meseguer, J., Multiparadigm logic programming, in: H. Kirchner and G. Levi, editors, Proc. 3rd Intl. Conf. on Algebraic and Logic Programming (1992), pp. 158-200 |

[45] | Meseguer, J., Membership algebra as a logical framework for equational specification, in: F. Parisi-Presicce, editor, Proc. WADT’97 (1998), pp. 18-61 · Zbl 0903.08009 |

[46] | Meseguer, J. and C. Talcott, Semantic models for distributed object reflection, in: Proceedings of ECOOP’02, Málaga, Spain, June 2002 (2002) · Zbl 1049.68815 |

[47] | Meseguer, J. and P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High-Order Symbolic Computation (2006), to appear · Zbl 1115.68079 |

[48] | Needham, R.; Schroeder, M., Using encryption for authentication in large networks of computers, Communications of the ACM, 21, 993-999, (1978) · Zbl 0387.68003 |

[49] | Nieuwenhuis, R., Basic paramodulation and decidable theories, in: Proceedings of the Eleventh Annual IEEE Symposium On Logic In Computer Science (LICS’96) (1996), pp. 473-483 |

[50] | Ohsaki, H.; Seki, H.; Takai, T., Recognizing Boolean closed A-tree languages with membership conditional mechanism, (), 483-498 · Zbl 1038.68070 |

[51] | Owre, S., N. Shankar, J. Rushby and D. Stringer-Calvert, “PVS system guide, PVS language reference, and PVS prover guide version 2.4,” Computer Science Laboratory, SRI International (2001) |

[52] | Paulson, L., Isabelle: A generic theorem prover, Lecture notes in computer science, 828, (1994), Springer Verlag · Zbl 0825.68059 |

[53] | Reddy, U., Term rewriting induction, (), 162-177 |

[54] | Saïdi, H.; Shankar, N., Abstract and model check while you prove, (), 443-454 · Zbl 1046.68608 |

[55] | Sekar, R.; Ramakrishnan, I., Programming in equational logic: beyond strong sequentiality, Information and computation, 104, 78-109, (1993) · Zbl 0803.68060 |

[56] | Sørensen, M.H.; Glück, R.; Jones, N.D., A positive supercompiler, Journal of functional programming, 6, 811-838, (1996) · Zbl 0870.68040 |

[57] | () |

[58] | Thati, P. and J. Meseguer, Complete symbolic reachability analysis using back-and-forth narrowing, Theoretical Computer Science (2006), to appear · Zbl 1110.68058 |

[59] | Turchin, V.F., Program transformation by supercompilation, (), 257-281 · Zbl 0587.68015 |

[60] | Viry, P., Equational rules for rewriting logic, Theoretical computer science, 285, 487-517, (2002) · Zbl 1001.68058 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.