{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:55Z","timestamp":1761611215801},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434191"},{"type":"electronic","value":"9783540460022"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_16","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T06:29:59Z","timestamp":1193552999000},"page":"221-235","source":"Crossref","is-referenced-by-count":15,"title":["Beyond Parameterized Verification"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giorgio","family":"Delzanno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS\u201996, pp. 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"16_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Verifying Networks of Timed Processes","author":"P. A. Abdulla","year":"1998","unstructured":"P. A. Abdulla and B. Jonsson. Verifying Networks of Timed Processes. In Proc. TACAS\u201998, LNCS 1384, pp. 298\u2013312, 1998."},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Channel Representations in Protocol Verification","author":"P. A. Abdulla","year":"2001","unstructured":"P. A. Abdulla and B. Jonsson. Channel Representations in Protocol Verification. In Proc. CONCUR\u20192001, LNCS 2154, p. 1\u201315, 2001."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla and A. Nyl\u00e9n. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proc. LICS\u201900, pp. 132\u2013140, 2000.","DOI":"10.1109\/LICS.2000.855762"},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Parameterized Verification with Automatically Computed Inductive Assertions","author":"T. Arons","year":"2001","unstructured":"T. Arons, A. Pnueli, S. Ruah, Y. Xu, and L. D. Zuck. Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. CAV\u201901, LNCS 2102, pp. 221\u2013234, 2001."},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-46419-0_14","volume-title":"Abstracting WS1S Systems to Verify Parameterized Networks","author":"K. Baukus","year":"2000","unstructured":"K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In Proc. TACAS\u201900, LNCS 1785, pp. 188\u2013203, 2000."},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Regular Model Checking","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular Model Checking. In Proc. CAV\u201900, LNCS 1855, pp. 403\u2013418, 2000."},{"key":"16_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetics","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetics. In Proc. CAV\u201997, LNCS 1254, pp. 400\u2013411, 1997."},{"key":"16_CR9","unstructured":"I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell, and A. Scedrov. A Metanotation for Protocol Analysis. In Proc. CSFW\u201999, p. 55\u201369, 1999."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Automatic Verification of Parameterized Cache Coherence Protocols","author":"G. Delzanno","year":"2000","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV\u201900, LNCS 1855, pp. 53\u201368, 2000."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"G. Delzanno. An Assertional Language for Systems Parametric in Several Dimensions. In Proc. VEPAS\u2019 01, ENTCS volume 50, issue 4, 2001.","DOI":"10.1016\/S1571-0661(04)00189-6"},{"key":"16_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Model checking in CLP","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in CLP. In Proc. TACAS\u201999, LNCS 1579, pp. 223\u2013239, 1999."},{"key":"16_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-44585-4_28","volume-title":"Attacking Symbolic State Explosion","author":"G. Delzanno","year":"2001","unstructured":"G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking Symbolic State Explosion. In Proc. CAV\u201901, LNCS 2102, pp. 298\u2013310, 2001."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. On Model Checking for Non-Deterministic Infinite-State Systems. In Proc. LICS\u201998, pp. 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS\u201999, pp. 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"16_CR16","unstructured":"F. Fioravanti, A. Pettorossi, M. Proietti. Verifcation of Sets of Infinite State Systems Using Program Transformation. In Proc. LOPSTR\u201901, pp. 55\u201366, 2001."},{"issue":"1","key":"16_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and P. Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science, 256(1\u20132):63\u201392, 2001.","journal-title":"Theoretical Computer Science"},{"key":"16_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/10720327_3","volume-title":"Constraint Logic Programming Applied to Model Checking","author":"L. Fribourg","year":"2000","unstructured":"L. Fribourg. Constraint Logic Programming Applied to Model Checking. In Proc. LOPSTR\u201999, LNCS 1817, pp. 30\u201341, 1999."},{"issue":"3","key":"16_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German and A. P. Sistla. Reasoning about Systems with Many Processes. Journal of the ACM, 39(3):675\u2013735, 1992.","journal-title":"Journal of the ACM"},{"key":"16_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/3-540-46419-0_16","volume-title":"Transitive Closures of Regular Relations for Verifying Infinite-State Systems","author":"B. Jonsson","year":"2000","unstructured":"B. Jonsson and M. Nilsson. Transitive Closures of Regular Relations for Verifying Infinite-State Systems. In Proc. TACAS\u201900, LNCS 1785, pp. 220\u2013234, 2000."},{"key":"16_CR21","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Symbolic model checking with rich assertional languages","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In Proc. CAV\u201997, LNCS 1254, pp. 424\u2013435, 1997."},{"key":"16_CR22","unstructured":"M. Nilsson. Regular Model Checking. PhD thesis, Department of Information Technology, Uppsala University, 2000."},{"key":"16_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/10722167_26","volume-title":"Liveness and Acceleration in Parameterized Verification","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and Acceleration in Parameterized Verification. In Proc. CAV\u201900, LNCS 1855, pp. 328\u2013343, 2000."},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01270929","volume":"6","author":"M. Rusinowitch","year":"1995","unstructured":"M. Rusinowitch and L. Vigneron. Automated Deduction with Associative and Commutative Operators. Applicable Algebra in Engineering, Communication and Computing, 6:23\u201356, 1995.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T01:11:04Z","timestamp":1548378664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}