{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T21:09:24Z","timestamp":1768511364263,"version":"3.49.0"},"reference-count":68,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T00:00:00Z","timestamp":1172275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,4,4]]},"DOI":"10.1007\/s10990-007-9000-6","type":"journal-article","created":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T03:23:38Z","timestamp":1172287418000},"page":"123-160","source":"Crossref","is-referenced-by-count":69,"title":["Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols"],"prefix":"10.1007","volume":"20","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[]},{"given":"Prasanna","family":"Thati","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,2,24]]},"reference":[{"key":"9000_CR1","doi-asserted-by":"crossref","unstructured":"Amadio R., Lugiez, D.: On the reachability problem in cryptographic primitives. In: Palamidessi, C. (ed.) 11th International Conference on Concurrency Theory (CONCUR \u201d00), vol. 1877 of Lecture Notes in Computer Science, pp. 380\u2013394. Springer (2000)","DOI":"10.1007\/3-540-44618-4_28"},{"key":"9000_CR2","doi-asserted-by":"crossref","unstructured":"Antoy, S.: Definitional trees. In: Proceedings of the 3rd International Conference on Algebraic and Logic Programming ALP\u201d92, vol. 632 of Lecture Notes in Computer Science, pp. 143\u2013157. Springer, Berlin (1992)","DOI":"10.1007\/BFb0013825"},{"key":"9000_CR3","doi-asserted-by":"crossref","unstructured":"Antoy, S., Echahed, R., Hanus, M.: Parallel evaluation strategies for functional logic languages. In: Proceedings of the Fourteenth International Conference on Logic Programming (ICLP\u201d97), pp. 138\u2013152. MIT Press (1997)","DOI":"10.7551\/mitpress\/4299.003.0016"},{"key":"9000_CR4","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1145\/347476.347484","volume":"474","author":"S. Antoy","year":"2000","unstructured":"Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776\u2013822 (2000)","journal-title":"J. ACM"},{"key":"9000_CR5","doi-asserted-by":"crossref","unstructured":"Antoy, S., Ariola, Z.M.: Narrowing the narrowing space. In: International Symposium on Programming Languages, Implementations, Logics, and Programs, vol. 1292 of Lecture Notes in Computer Science, pp. 1\u201315. Springer (1997)","DOI":"10.1007\/BFb0033833"},{"key":"9000_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D., Modersheim, S., Vigano, L.: Constraint differentiation: A new reduction technique for constraint-based analysis of security protocols. Technical Report TR-405, Swiss Federal Institute of Technology, Zurich (May 2003)","DOI":"10.1145\/948109.948154"},{"key":"9000_CR7","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01202035","volume":"43","author":"A. Bockmayr","year":"1993","unstructured":"Bockmayr, A.: Conditional narrowing modulo of set of equations. Appl. Algebra Eng. Commun. Comput. 4(3), 147\u2013168 (1993)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9000_CR8","doi-asserted-by":"crossref","unstructured":"Bockmayr, A., Krischer, S., Werner, A.: An optimal narrowing strategy for general canonical systems. In: Rusinowitch, M., R\u00e9my, J.L. (eds.) 3rd International Workshop on Conditional Term Rewrite systems, vol. 656 of Lecture Notes in Computer Science, pp. 483\u2013497. Springer (1992)","DOI":"10.1007\/3-540-56393-8_39"},{"key":"9000_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) 16th Annual Symposium on Theoretical Aspects of Computer Science, vol. 1563 of Lecture Notes in Computer Science, pp. 323\u2013333 (1999)","DOI":"10.1007\/3-540-49116-3_30"},{"key":"9000_CR10","doi-asserted-by":"crossref","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification over infinite states. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 545\u2013623. Elsevier Publishing (2001)","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"9000_CR11","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P., Radhakrishnan, J. (eds.) 23rd Conference on Foundations Software Technology and Theoretical Computer Science, vol. 2914 of Lecture Notes in Computer Science. Springer (2003)","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"9000_CR12","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS \u201d03), pp. 261\u2013270 (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"9000_CR13","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"9000_CR14","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"165","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9000_CR15","unstructured":"Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications (2000)"},{"key":"9000_CR16","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285, 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9000_CR17","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (version 2.2) (Dec. 2005)"},{"key":"9000_CR18","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS \u201d03), pp. 271\u2013280 (2003)","DOI":"10.1109\/LICS.2003.1210067"},{"key":"9000_CR19","unstructured":"Denker, G., Meseguer, J., Talcott, C.L.: Protocol specification and analysis in Maude. In: Heintze, N., Wing, J. (eds.) Proceedings of Workshop on Formal Methods and Security Protocols, June 25, 1998, Indianapolis, Indiana (1998)"},{"key":"9000_CR20","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"292","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"9000_CR21","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Lincoln, P., Meseguer, J.: Principles of Mobile Maude. In: Agent Systems, Mobile Agents, and Applications, ASA\/MA 2000, vol. 1882 of Lecture Notes in Computer Science, pp. 73\u201385. Springer (2000)","DOI":"10.1007\/978-3-540-45347-5_7"},{"key":"9000_CR22","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of Bounded Security Protocols. In: Workshop on formal methods and security protocols, FMSP (1999)"},{"key":"9000_CR23","doi-asserted-by":"crossref","unstructured":"Emerson, A., Namjoshi, K.: On model checking for nondeterministic infinite state systems. In: 13th IEEE Symposium on Logic in Computer Science, pp. 70\u201380 (1998)","DOI":"10.1109\/LICS.1998.705644"},{"key":"9000_CR24","doi-asserted-by":"crossref","unstructured":"Escobar, S.: Refining weakly outermost-needed rewriting and narrowing. In: Miller, D. (ed.) Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP\u201d03, pp. 113\u2013123. ACM Press, New York (2003)","DOI":"10.1145\/888251.888263"},{"key":"9000_CR25","doi-asserted-by":"crossref","unstructured":"Escobar, S.: Implementing natural rewriting and narrowing efficiently. In: Kameyama, Y., Stuckey, P.J. (eds.) 7th International Symposium on Functional and Logic Programming (FLOPS 2004), vol. 2998 of Lecture Notes in Computer Science, pp. 147\u2013162. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24754-8_12"},{"key":"9000_CR26","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer: Grammar generation. In: Proceedings of the 3rd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code. ACM Press (2005)","DOI":"10.1145\/1103576.1103578"},{"key":"9000_CR27","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) 16th International Conference on Rewriting Techniques and Applications, vol. 3467 of Lecture notes in computer science, pp. 279\u2013293. Springer (2005)","DOI":"10.1007\/978-3-540-32033-3_21"},{"key":"9000_CR28","unstructured":"Fay, M.: First order unification in equational theories. In: Bibel, W., Kowalski, R. (eds.) 4th Conference on Automated Deduction, vol. 87 of Lecture Notes in Computer Science, pp. 161\u2013167. Springer (1979)"},{"key":"9000_CR29","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"2561","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"9000_CR30","doi-asserted-by":"crossref","unstructured":"Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAllester, D. (ed.) Automated Deduction\u2014CADE 17, vol. 1831 of Lecture notes in artificial intelligence, pp. 271\u2013290. Springer (2000)","DOI":"10.1007\/10721959_21"},{"key":"9000_CR31","doi-asserted-by":"crossref","unstructured":"Genet, T., Tong, V.V.T.: Reachability analysis of term rewriting systems with Timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) 8th International Conference on Logic for Programming, vol. 2250 of Lecture Notes in Computer Science, pp. 695\u2013706 (2001)","DOI":"10.1007\/3-540-45653-8_48"},{"key":"9000_CR32","doi-asserted-by":"crossref","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) Computer Aided Verification. 9th International Conference, CAV\u201d97, Haifa, Israel, June 22\u201325, 1997, Proceedings, vol. 1254 of Lecture Notes in Computer Science, pp. 72\u201383. Springer (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"9000_CR33","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"1920","author":"M. Hanus","year":"1994","unstructured":"Hanus, M.: The integration of functions into logic programming: From theory to practice. J. Log. Program. 19(20), 583\u2013628 (1994)","journal-title":"J. Log. Program."},{"key":"9000_CR34","unstructured":"Huet, G., L\u00e9vy, J.-J.: Computations in Orthogonal Term Rewriting Systems, Part I + II. In: Computational logic: Essays in honour of J. Alan Robinson, pp. 395\u2013414 and 415\u2013443. The MIT Press, Cambridge, MA (1992)"},{"key":"9000_CR35","unstructured":"Huima, A.: Efficient infinite state analysis of security protocols. In: Workshop on Formal Methods and Security Protocols, FMSP (1999)"},{"key":"9000_CR36","doi-asserted-by":"crossref","unstructured":"Hullot, J.M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) 5th Conference on Automated Deduction, vol. 87 of Lecture Notes in Computer Science, pp. 318\u2013334. Springer (1980)","DOI":"10.21236\/ADA087640"},{"key":"9000_CR37","doi-asserted-by":"crossref","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) Logic Programming and Automated Reasoning, vol. 1955 of Lecture Notes in Computer Science, pp. 131\u2013160. Springer (2000)","DOI":"10.1007\/3-540-44404-1_10"},{"key":"9000_CR38","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: 10th International Colloquium on Automata, Languages and Programming, vol. 154 of Lecture Notes in Computer Science, pp. 361\u2013373. Springer (1983)","DOI":"10.1007\/BFb0036921"},{"key":"9000_CR39","doi-asserted-by":"crossref","unstructured":"Kapur, D., Narendran, P., Wang, L.: An e-unification algorithm for analyzing protocols that use modular exponentiation. In: Nieuwenhuis, R. (ed.) International Conference on Rewriting Techniques and Applications (RTA\u201d03), vol. 2706 of Lecture Notes in Computer Science, pp. 165\u2013179. Springer (2003)","DOI":"10.1007\/3-540-44881-0_13"},{"key":"9000_CR40","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/s100090050040","volume":"42","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Int. J. Softw. Tools Technol. Transfer 4(2), 328\u2013342 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9000_CR41","doi-asserted-by":"crossref","unstructured":"Kirchner, H.: On the use of constraints in automated deduction. In: Podelski, A. (ed.) Constraint Programming: Basics and Trends, pp. 128\u2013146. Springer LNCS 910 (1995)","DOI":"10.1007\/3-540-59155-9_8"},{"key":"9000_CR42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6, 1\u201336 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"9000_CR43","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Steffen, B., Margaria, T. (eds.) Tools and algorithms for construction and analysis of systems (TACAS \u201d96), vol. 1055 of Lecture Notes in Computer Science, pp. 147\u2013166. Springer (1996).","DOI":"10.1007\/3-540-61042-1_43"},{"key":"9000_CR44","doi-asserted-by":"crossref","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd. Edn., pp. 1\u201387. Kluwer Academic Publishers (2002). First published as SRI Tech. Report SRI-CSL-93-05 (Aug. 1993)","DOI":"10.1007\/978-94-017-0464-9_1"},{"issue":"2","key":"9000_CR45","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. J. Log. Program. 26(2), 113\u2013131 (1996)","journal-title":"J. Log. Program."},{"issue":"2","key":"9000_CR46","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. J. Log. program. 26(2), 113\u2013131 (1996)","journal-title":"J. Log. program"},{"key":"9000_CR47","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Localized fairness: A rewriting semantics. In: Giesl, J. (ed.) International Conference on Term Rewriting and Applications, vol. 3467 of Lecture Notes in Computer Science, pp. 250\u2013263. Springer (2005)","DOI":"10.1007\/978-3-540-32033-3_19"},{"key":"9000_CR48","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) Proceedings of ECOOP\u201d02, M\u00e1laga, Spain, June 2002, pp. 1\u201336. Springer LNCS 2374 (2002)","DOI":"10.1007\/3-540-47993-7_1"},{"key":"9000_CR49","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and it application to verification of cryptographic protocols. In: Mart\u00ed-Oliet, N. (ed.) International Workshop on Rewriting Logic and its Application, WRLA\u201d04, vol. 117 of Electronic Notes in Theoretical Computer Science, pp. 153\u2013182. Elsevier Sciences Publisher (2004)","DOI":"10.1016\/j.entcs.2004.06.024"},{"issue":"1","key":"9000_CR50","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"9000_CR51","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In:Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. The MIT Press (1993)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"9000_CR52","doi-asserted-by":"crossref","unstructured":"Meseguer, J. Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) International Workshop on Algebraic Development Techniques, vol. 1376 of Lecture Notes in Computer Science, pp. 18\u201361. Springer (1998)","DOI":"10.1007\/3-540-64299-4_26"},{"key":"9000_CR53","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security (CCS \u201d01), pp. 166\u2013175 (2001)","DOI":"10.1145\/502006.502007"},{"key":"9000_CR54","doi-asserted-by":"crossref","unstructured":"Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In: 16th IEEE Computer Security Foundations Workshop (CSFW-16), pp. 47\u201361 (2003)","DOI":"10.1109\/CSFW.2003.1212704"},{"key":"9000_CR55","unstructured":"Narendran, P., Meadows, C.: A unification algorithm for the group Diffie-Hellman protocol. In: Workshop on Issues in the Theory of Security (WITS\u201d02) (2002)"},{"key":"9000_CR56","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.: On narrowing, refutation proofs and constraints. In: Hsiang, J. (ed.) 6th International Conference on Rewriting Techniques and Applications, vol. 914, pp. 56\u201370. Springer LNCS (1995)","DOI":"10.1007\/3-540-59200-8_47"},{"key":"9000_CR57","doi-asserted-by":"crossref","unstructured":"Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed A-tree languages with membership conditional mechanism. In: Nieuwenhuis, R. (ed.) 14th International Conference on Rewriting Techniques and Applications, vol. 2706 of Lecture notes in computer science, pp. 483\u2013498. Springer (2003)","DOI":"10.1007\/3-540-44881-0_34"},{"key":"9000_CR58","unstructured":"Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS system guide, PVS language reference, and PVS prover guide version 2.4. Computer Science Laboratory, SRI International (2001)"},{"key":"9000_CR59","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"9000_CR60","doi-asserted-by":"crossref","unstructured":"Ramos, J.G., Silva, J., Vidal, G.: Fast Narrowing-Driven Partial Evaluation for Inductively Sequential Systems. In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005), pp. 228\u2013239. ACM Press (2005)","DOI":"10.1145\/1090189.1086394"},{"key":"9000_CR61","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. In: 14th IEEE Computer Security Foundations Workshop, pp. 174\u2013190 (2001)","DOI":"10.1109\/CSFW.2001.930145"},{"key":"9000_CR62","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S0020-0190(97)00180-4","volume":"65","author":"P. Ryan","year":"1998","unstructured":"Ryan, P., Schneider, S.: An attack on a recursive authentication protocol. Inf. Process. Lett. 65, 7\u201310 (1998)","journal-title":"Inf. Process. Lett."},{"key":"9000_CR63","doi-asserted-by":"crossref","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D. (eds.) Computer Aided Verification. 11th International Conference, CAV\u201d99, Trento, Italy, July 6\u201310, 1999, Proceedings, vol. 1633 of Lecture Notes in Computer Science, pp. 443\u2013454. Springer (1999)","DOI":"10.1007\/3-540-48683-6_38"},{"issue":"1","key":"9000_CR64","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1006\/inco.1993.1026","volume":"104","author":"R.C. Sekar","year":"1993","unstructured":"Sekar, R.C., Ramakrishnan, I.V.: Programming in equational logic: Beyond strong sequentiality. Inf. Comput. 104(1), 78\u2013109 (1993)","journal-title":"Inf. Comput."},{"key":"9000_CR65","doi-asserted-by":"crossref","unstructured":"Stehr, M.-O., Meseguer, J., \u00d6lveczky, P.: Rewriting logic as a unifying framework for Petri nets. In: Unifying Petri Nets, vol. 2128 of Lecture Notes in Computer Science, pp. 250\u2013303. Springer (2001)","DOI":"10.1007\/3-540-45541-8_9"},{"key":"9000_CR66","doi-asserted-by":"crossref","unstructured":"Thati, P., Meseguer, J.: Complete symbolic reachability analysis using back-and-forth narrowing. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds.) Conference on Algebra and Co-algebra in Computer Science, vol. 3629 of Lecture Notes in Computer Science, pp. 379\u2013394. Springer (2005)","DOI":"10.1007\/11548133_24"},{"key":"9000_CR67","doi-asserted-by":"crossref","unstructured":"Takai, T.: A verification technique using term rewriting systems and abstract interpretation. In: Halatsis et al., (eds.) Proceedings RTA 2004, vol. 3091 of Lecture Notes in Computer Science, pp. 119\u2013133. Springer (2004)","DOI":"10.1007\/978-3-540-25979-4_9"},{"key":"9000_CR68","doi-asserted-by":"crossref","unstructured":"Viry, P.: Rewriting: An effective model of concurrency. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE\u201d94 Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4\u20138, 1994, Proceedings, vol. 817 of Lecture Notes in Computer Science, pp. 648\u2013660. Springer (1994)","DOI":"10.1007\/3-540-58184-7_138"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9000-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9000-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9000-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,14]],"date-time":"2025-01-14T04:16:32Z","timestamp":1736828192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9000-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,24]]},"references-count":68,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,4,4]]}},"alternative-id":["9000"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9000-6","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2,24]]}}}