{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:57:44Z","timestamp":1725569864743},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_22","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T17:40:06Z","timestamp":1289238006000},"page":"321-337","source":"Crossref","is-referenced-by-count":5,"title":["Automated Multiparameterised Verification by Cut-Offs"],"prefix":"10.1007","author":[{"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"6","key":"22_CR1","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"22_CR2","series-title":"LNCS","first-page":"561","volume-title":"ICFEM 2009","author":"A. Siirtola","year":"2009","unstructured":"Siirtola, A., Kortelainen, J.: Algorithmic verification with multiple and nested parameters. In: ICFEM 2009. LNCS, vol.\u00a05885, pp. 561\u2013580. Springer, Heidelberg (2009)"},{"key":"22_CR3","unstructured":"McKay, B.D.: Nauty User\u2019s Guide (Version 2.4). Department of Computer Science, Australian National University (2007)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume-title":"CONCUR 2004 - Concurrency Theory","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 276\u2013291. Springer, Heidelberg (2004)"},{"key":"22_CR5","first-page":"3","volume-title":"PSTV 1991","author":"A. Valmari","year":"1991","unstructured":"Valmari, A., Tienari, M.: An improved failures equivalence for finite-state systems with a reduction algorithm. In: PSTV 1991, pp. 3\u201318. North-Holland, Amsterdam (1991)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-46002-0_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2002","unstructured":"Emerson, E.A., Kahlon, V.: Model checking large-scale and parameterized resource allocation systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 251\u2013265. Springer, Heidelberg (2002)"},{"issue":"4","key":"22_CR9","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci.\u00a014(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-30124-0_26","volume-title":"Computer Science Logic","author":"E.A. Emerson","year":"2004","unstructured":"Emerson, E.A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 325\u2013339. Springer, Heidelberg (2004)"},{"issue":"2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/32.265633","volume":"20","author":"J. Li","year":"1994","unstructured":"Li, J., Suzuki, I., Yamashita, M.: A new structural induction theorem for rings of temporal Petri nets. IEEE Trans. Softw. Eng.\u00a020(2), 115\u2013126 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"22_CR12","unstructured":"Pyssysalo, T.: An induction theorem for ring protocols of processes described with predicate\/transition nets. Research Report A37, Helsinki University of Technology (1996)"},{"issue":"2","key":"22_CR13","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10703-008-0048-7","volume":"32","author":"A. Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritised FIFO resource management. Form. Method. Syst. Des.\u00a032(2), 129\u2013172 (2008)","journal-title":"Form. Method. Syst. Des."},{"key":"22_CR14","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., Begin, L.V.: Towards the automated verification of multithreaded Java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-31980-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.D. Bingham","year":"2005","unstructured":"Bingham, J.D., Hu, A.J.: Empirically efficient verification for a class of infinite-state systems. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 77\u201392. Springer, Heidelberg (2005)"},{"key":"22_CR16","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"22_CR17","volume-title":"Communicating sequential processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Siirtola, A.: Algorithmic Multiparameterised Verification of Safety Properties. Process Algebraic Approach. PhD thesis, University of Oulu (2010)","DOI":"10.1007\/978-3-642-16901-4_22"},{"key":"22_CR19","first-page":"105","volume-title":"ACSD 2010","author":"A. Siirtola","year":"2010","unstructured":"Siirtola, A.: Cut-offs with network invariants. In: ACSD 2010, pp. 105\u2013114. IEEE, Los Alamitos (2010)"},{"key":"22_CR20","series-title":"Algorithms and Computation in Mathematics","volume-title":"Classification Algorithms for Codes and Designs","author":"P. Kaski","year":"2006","unstructured":"Kaski, P., \u00d6sterg\u00e5rd, P.R.J.: Classification Algorithms for Codes and Designs. Algorithms and Computation in Mathematics, vol.\u00a015. Springer, Heidelberg (2006)"},{"issue":"1","key":"22_CR21","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.datak.2007.11.001","volume":"65","author":"M. Haustein","year":"2008","unstructured":"Haustein, M., H\u00e4rder, T.: Optimizing lock protocols for native XML processing. Data Knowl. Eng.\u00a065(1), 147\u2013173 (2008)","journal-title":"Data Knowl. Eng."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T04:12:17Z","timestamp":1559794337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}