{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:16:46Z","timestamp":1794349006778,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540742395","type":"print"},{"value":"9783540742401","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74240-1_1","type":"book-chapter","created":{"date-parts":[[2007,8,27]],"date-time":"2007-08-27T07:04:18Z","timestamp":1188198258000},"page":"1-22","source":"Crossref","is-referenced-by-count":33,"title":["Rewriting Systems with Data"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yan","family":"Jurski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45740-2_5","volume-title":"Applications and Theory of Petri Nets 2001","author":"P. Abdulla","year":"2001","unstructured":"Abdulla, P., Nylen, A.: Timed Petri Nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075. Springer, Heidelberg (2001)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. of LICS 1996, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"1_CR3","volume-title":"Proc. of AVIS\u201906, Satellite workshop of ETAPS 2006","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Delzanno, G.: On the Coverability Problem for Constrained Multiset Rewriting. In: Proc. of AVIS\u201906, Satellite workshop of ETAPS 2006, Vienna, Austria (2006)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A Survey of Regular Model Checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170. Springer, Heidelberg (2004)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054179","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes (extended abstract). In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384. Springer, Heidelberg (1998)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_32","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2000","unstructured":"Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102. Springer, Heidelberg (2001)"},{"key":"1_CR8","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Space. PhD thesis, Facult\u00e9 des Sciences, Universit\u00e9 de Li\u00e8ge, vol. 189 (1999)"},{"key":"1_CR9","volume-title":"Proc. of PODS 2006","author":"M. Bojanczyk","year":"2006","unstructured":"Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and XML reasoning. In: Proc. of PODS 2006, ACM Press, New York (2006)"},{"key":"1_CR10","volume-title":"Proc. of LICS 2006","author":"M. Bojanczyk","year":"2006","unstructured":"Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: Proc. of LICS 2006, IEEE, New York (2006)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 Infinte-State Systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076. Springer, Heidelberg (2001)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists Are Counter Automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144. Springer, Heidelberg (2006)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_11","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Esparza, J.: Rewriting Models for Boolean Programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098. Springer, Heidelberg (2006)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 1997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Technology for Verification and Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Tree Regular Model Checking of Complex Dynamic Data Structures. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218. Springer, Heidelberg (2006)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: TACAS 2007. LNCS (2007)","DOI":"10.1007\/978-3-540-71209-1_54"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Mayr, R.: Automatic Verification of Recursive Procedures with one Integer Parameter. Theoretical Computer Science\u00a0295 (2003)","DOI":"10.1016\/S0304-3975(02)00397-3"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Beyond Parameterized Verification. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280. Springer, Heidelberg (2002)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855. Springer, Heidelberg (2005)"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: An assertional language for the verification of systems parametric in several dimensions. Electr. Notes Theor. Comput. Sci.\u00a050(4) (2001)","DOI":"10.1016\/S1571-0661(04)00189-6"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Constraint-based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design\u00a023(3) (2003)","DOI":"10.1023\/A:1026276129010"},{"key":"1_CR24","volume-title":"Proc. of LICS 2006","author":"S. Demri","year":"2006","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. In: Proc. of LICS 2006, IEEE, New York (2006)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02556. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"1_CR26","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, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci.\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Habermehl","year":"2006","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: Automata-Based Verification of Programs with Tree Updates. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920. Springer, Heidelberg (2006)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74240-1_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:14:54Z","timestamp":1619504094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74240-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540742395","9783540742401"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74240-1_1","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-74240-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}