{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:19:05Z","timestamp":1725560345032},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540286202"},{"type":"electronic","value":"9783540318767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11548133_24","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T16:07:40Z","timestamp":1279728460000},"page":"379-394","source":"Crossref","is-referenced-by-count":5,"title":["Complete Symbolic Reachability Analysis Using Back-and-Forth Narrowing"],"prefix":"10.1007","author":[{"given":"Prasanna","family":"Thati","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"24_CR1","doi-asserted-by":"publisher","first-page":"776","DOI":"10.1145\/347476.347484","volume":"47","author":"S. Antoy","year":"2000","unstructured":"Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. Journal of the ACM\u00a047(4), 776\u2013822 (2000)","journal-title":"Journal of the ACM"},{"key":"24_CR2","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 Insititute of Technology, Zurich (May 2003)","DOI":"10.1145\/948109.948154"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/3-540-45657-0_46","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2002","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 539. Springer, Heidelberg (2002)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1016\/B978-044482830-9\/50027-8","volume-title":"Handbook of Process Algebra","author":"O. Burkart","year":"2001","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification over Infinite States. In: Handbook of Process Algebra, pp. 545\u2013623. Elsevier Publishing, Amsterdam (2001)"},{"issue":"2","key":"24_CR5","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transaction on Information Theory\u00a029(2), 198\u2013208 (1983)","journal-title":"IEEE Transaction on Information Theory"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: International Conference on Rewriting Techniques and applications (RTA) (2005); also available at, http:\/\/www.dsic.upc.es\/users\/elp\/papers.html","DOI":"10.1007\/978-3-540-32033-3_21"},{"issue":"1","key":"24_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/10721959_21","volume-title":"Automated Deduction - CADE-17","author":"T. Genet","year":"2000","unstructured":"Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 271\u2013290. Springer, Heidelberg (2000)"},{"issue":"20","key":"24_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19","author":"M. Hanus","year":"1994","unstructured":"Hanus, M.: The integration of functions into logic programming: From theory to practice. Jounral of Logic Programming\u00a019(20), 583\u2013628 (1994)","journal-title":"Jounral of Logic Programming"},{"key":"24_CR10","series-title":"ENTCS","volume-title":"Proc. 5th Intl. Workshop on Rule-Based Programming (RULE 2004)","author":"H. Seki","year":"2004","unstructured":"Seki, H., Ohsaki, H., Takai, T.: ACTAS: A system design for associative and commutative tree automata theory. In: Proc. 5th Intl. Workshop on Rule-Based Programming (RULE 2004). ENTCS, Elsevier, Amsterdam (2004)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.M. Hullot","year":"1980","unstructured":"Hullot, J.M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) 5th Conference on Automated Deduction. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0036921","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 361\u2013373. Springer, Heidelberg (1983)"},{"issue":"2","key":"24_CR13","doi-asserted-by":"publisher","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. Journal of logic programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of logic programming"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to analysis of cryptographic protocols. In: Workshop on Rewriting Logic and its Applications. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2004), also available at http:\/\/osl.cs.uiuc.edu\/docs\/wrla04\/main.ps (to appear)","DOI":"10.1016\/j.entcs.2004.06.024"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0013830","volume-title":"Algebraic and Logic Programming","author":"A. Middeldorp","year":"1992","unstructured":"Middeldorp, A., Hamoen, E.: Counterexamples to completeness results for basic narrowing. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 244\u2013258. Springer, Heidelberg (1992)"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Okui, S., Middeldorp, A., Ida, T.: Lazy narrowing: Strong completeness and eager variable elimination. In: Proceedings of the 20th Colloquium on Trees in Algebra and Programming. LNCS, vol.\u00a0915, pp. 394\u2013408 (1995)","DOI":"10.1007\/3-540-59293-8_209"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"G.E. Peterson","year":"1978","unstructured":"Peterson, G.E., Wegman, M.N.: Linear unification. Journal of Computer and Systems Sciences\u00a016, 158\u2013167 (1978)","journal-title":"Journal of Computer and Systems Sciences"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-540-25979-4_9","volume-title":"Rewriting Techniques and Applications","author":"T. Takai","year":"2004","unstructured":"Takai, T.: A verification technique using term rewriting systems and abstract interpretation. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 119\u2013133. Springer, Heidelberg (2004)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/10721975_17","volume-title":"Rewriting Techniques and Applications","author":"T. Takai","year":"2000","unstructured":"Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 246\u2013260. Springer, Heidelberg (2000)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Algebra and Coalgebra in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11548133_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T20:59:47Z","timestamp":1635713987000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11548133_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540286202","9783540318767"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11548133_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}