{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T22:59:36Z","timestamp":1765666776601},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540734475"},{"type":"electronic","value":"9783540734499"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73449-9_13","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T16:49:53Z","timestamp":1187023793000},"page":"153-168","source":"Crossref","is-referenced-by-count":45,"title":["Symbolic Model Checking of Infinite-State Systems Using Narrowing"],"prefix":"10.1007","author":[{"given":"Santiago","family":"Escobar","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"13_CR1","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1145\/291891.291896","volume":"20","author":"M. Alpuente","year":"1998","unstructured":"Alpuente, M., Falaschi, M., Vidal, G.: Partial Evaluation of Functional Logic Programs. ACM TOPLAS\u00a020(4), 768\u2013844 (1998)","journal-title":"ACM TOPLAS"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0033833","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"S. Antoy","year":"1997","unstructured":"Antoy, S., Ariola, Z.M.: Narrowing the narrowing space. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol.\u00a01292, pp. 1\u201315. Springer, Heidelberg (1997)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45635-X_19","volume-title":"Logic Programming","author":"S. Basu","year":"2001","unstructured":"Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.M.: Local and symbolic bisimulation using tabled constraint logic programming. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol.\u00a02237, pp. 166\u2013180. Springer, Heidelberg (2001)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-48224-5_3","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2001","unstructured":"Bouajjani, A.: Languages, rewriting systems, and verification of infinite-state systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 24\u201339. Springer, Heidelberg (2001)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/11805618_11","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Esparza, J.: Rewriting models of boolean programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 136\u2013150. Springer, Heidelberg (2006)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"STACS 1999","author":"A. Bouajjani","year":"1999","unstructured":"Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol.\u00a01563, pp. 323\u2013333. Springer, Heidelberg (1999)"},{"key":"13_CR7","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, Amsterdam (2001)"},{"issue":"5","key":"13_CR8","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM TOPLAS\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM TOPLAS"},{"key":"13_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"13_CR10","volume-title":"All About Maude: A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude: A High-Performance Logical Framework. Springer, Heidelberg (To appear 2007)"},{"key":"13_CR11","unstructured":"Delzanno, G.: Constraint multiset rewriting. Technical report, DISI - Universit\u00e0 di Genova (2002)"},{"issue":"3","key":"13_CR12","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/s100090100049","volume":"3","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Podelski, A.: Constraint-based deductive model checking. STTT\u00a03(3), 250\u2013270 (2001)","journal-title":"STTT"},{"key":"13_CR13","unstructured":"Denker, G., Meseguer, J., Talcott, C.L.: Protocol specification and analysis in Maude. In: Proc. of Workshop on Formal Methods and Security Protocols (1998)"},{"key":"13_CR14","first-page":"70","volume-title":"LICS 1998","author":"A. Emerson","year":"1998","unstructured":"Emerson, A., Namjoshi, K.: On model checking for nondeterministic infinite state systems. In: LICS 1998, pp. 70\u201380. IEEE Press, New York (1998)"},{"issue":"1-2","key":"13_CR15","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S. Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theoretical Computer Science (Elsevier) 367(1-2), 162\u2013202 (2006)","journal-title":"Theoretical Computer Science"},{"key":"13_CR16","unstructured":"Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. Technical Report No. 2814, Department of Computer Science, University of Illinois at Urbana-Champaign (2007)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11784180_13","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2006","unstructured":"Farzan, A., Meseguer, J.: State space reduction of rewrite theories using invisible transitions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 142\u2013157. Springer, Heidelberg (2006)"},{"issue":"1","key":"13_CR18","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":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1007\/3-540-45653-8_48","volume-title":"ICLP 2001","author":"T. Genet","year":"2001","unstructured":"Genet, T., Viet Triem Tong, V.: Reachability analysis of term rewriting systems with Timbuk. In: LPAR 2001. LNCS, vol.\u00a02250, pp. 695\u2013706. Springer, Heidelberg (2001)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"2","key":"13_CR21","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. STTT\u00a04(2), 328\u2013342 (2000)","journal-title":"STTT"},{"key":"13_CR22","doi-asserted-by":"publisher","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. Formal Methods in System Design\u00a06, 1\u201336 (1995)","journal-title":"Formal Methods in System Design"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-31959-7_8","volume-title":"Recent Trends in Algebraic Development Techniques","author":"N. Mart\u00ed-Oliet","year":"2005","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J., Palomino, M.: Theoroidal maps as algebraic simulations. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol.\u00a03423, pp. 126\u2013143. Springer, Heidelberg (2005)"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High-Order Symbolic Computation (to appear, 2007)","DOI":"10.1007\/s10990-007-9000-6"},{"issue":"1","key":"13_CR25","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/BFb0013826","volume-title":"ALP 1992","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 158\u2013200. Springer, Heidelberg (1992)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"13_CR28","unstructured":"Meseguer, J.: The Temporal Logic of Rewriting. Technical Report No. 2815, Department of Computer Science, University of Illinois at Urbana-Champaign (2007)"},{"key":"13_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-45085-6_2","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Meseguer","year":"2003","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 2\u201316. Springer, Heidelberg (2003)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-44881-0_34","volume-title":"Rewriting Techniques and Applications","author":"H. Ohsaki","year":"2003","unstructured":"Ohsaki, H., Seki, H., Takai, T.: Recognizing boolean closed A-tree languages with membership conditional mechanism. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 483\u2013498. Springer, Heidelberg (2003)"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"13_CR32","volume-title":"Term Rewriting Systems","author":"TeReSe","year":"2003","unstructured":"TeReSe, (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/978-3-540-31980-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Vardhan","year":"2005","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Using language inference to verify omega-regular properties. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 45\u201360. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73449-9_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:14:49Z","timestamp":1605762889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73449-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540734475","9783540734499"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73449-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}