{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:40Z","timestamp":1725540520589},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_29","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"561-580","source":"Crossref","is-referenced-by-count":4,"title":["Algorithmic Verification with Multiple and Nested Parameters"],"prefix":"10.1007","author":[{"given":"Antti","family":"Siirtola","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juha","family":"Kortelainen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"6","key":"29_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":"29_CR2","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":"29_CR3","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":"29_CR4","first-page":"158","volume-title":"ACSD 2009","author":"A. Siirtola","year":"2009","unstructured":"Siirtola, A., Kortelainen, J.: Parameterised process algebraic verification by precongruence reduction. In: ACSD 2009, pp. 158\u2013167. IEEE, Los Alamitos (2009)"},{"issue":"2","key":"29_CR5","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":"29_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":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"29_CR8","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/512644.512661","volume-title":"POPL 1986","author":"P. Wolper","year":"1986","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL 1986, pp. 184\u2013193. ACM, New York (1986)"},{"key":"29_CR9","unstructured":"Lazi\u0107, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University (2001)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R.S. Lazi\u0107","year":"2000","unstructured":"Lazi\u0107, R.S., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 581\u2013595. Springer, Heidelberg (2000)"},{"issue":"4","key":"29_CR11","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":"29_CR12","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)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"29_CR14","first-page":"187","volume-title":"ACSD 2007","author":"S. Nazari","year":"2007","unstructured":"Nazari, S., Thistle, J.: Structural conditions for model-checking of parameterized networks. In: ACSD 2007, pp. 187\u2013196. IEEE, Los Alamitos (2007)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"5","key":"29_CR16","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s11086-005-0034-4","volume":"31","author":"I.V. Konnov","year":"2005","unstructured":"Konnov, I.V., Zakharov, V.A.: An approach to the verification of symmetric parameterized distributed systems. Program. Comput. Soft.\u00a031(5), 225\u2013236 (2005)","journal-title":"Program. Comput. Soft."},{"issue":"2","key":"29_CR17","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":"29_CR18","unstructured":"Pyssysalo, T.: An induction theorem for ring protocols of processes described with predicate\/transition nets. Research Report A37, Helsinki University of Technology (1996)"},{"key":"29_CR19","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":"29_CR20","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":"29_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"1","key":"29_CR22","doi-asserted-by":"crossref","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."},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-77566-9_40","volume-title":"SOFSEM 2008: Theory and Practice of Computer Science","author":"A. Siirtola","year":"2008","unstructured":"Siirtola, A., Valenta, M.: Verifying parameterized taDOM+ lock managers. In: Geffert, V., Karhum\u00e4ki, J., Bertoni, A., Preneel, B., N\u00e1vrat, P., Bielikov\u00e1, M. (eds.) SOFSEM 2008. LNCS, vol.\u00a04910, pp. 460\u2013472. Springer, Heidelberg (2008)"}],"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-10373-5_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:28:52Z","timestamp":1619782132000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}