{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T02:53:12Z","timestamp":1768272792928,"version":"3.49.0"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_21","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"685-725","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Model Checking Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. Prasad","family":"Sistla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muralidhar","family":"Talupur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"21_CR1","volume-title":"ACM Transactions on Programming Languages and Systems","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. In: ACM Transactions on Programming Languages and Systems. ACM, New York (1993)"},{"key":"21_CR2","first-page":"313","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0313\u2013321. IEEE, Piscataway (1996)"},{"key":"21_CR3","series-title":"LNCS","first-page":"721","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04424, pp.\u00a0721\u2013736. Springer, Heidelberg (2007)"},{"key":"21_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"P.A. Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u2019ik, L.: All for the price of few (parameterized verification through view abstraction). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a07737, pp.\u00a0476\u2013495. Springer, Heidelberg (2013)"},{"key":"21_CR5","series-title":"LNCS","first-page":"116","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jancar, P., Kret\u00ednsk\u00fd, M., Kucera, A. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02421, pp.\u00a0116\u2013130. Springer, Heidelberg (2002)"},{"key":"21_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-27813-9_27","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03114, pp.\u00a0348\u2013360. Springer, Heidelberg (2004)"},{"key":"21_CR7","series-title":"LNCS","first-page":"35","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a03170, pp.\u00a035\u201348. Springer, Heidelberg (2004)"},{"issue":"6","key":"21_CR8","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.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"21_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0221\u2013234. Springer, Heidelberg (2001)"},{"key":"21_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-47813-2_22","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"K. Baukus","year":"2002","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol: safety and liveness. In: Cortesi, A. (ed.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a02294, pp.\u00a0317\u2013330. Springer, Heidelberg (2002)"},{"key":"21_CR11","series-title":"LNCS","volume-title":"Intl. Symposium on Model Checking of Software (SPIN)","author":"R. Bhattacharya","year":"2006","unstructured":"Bhattacharya, R., German, S.M., Gopalakrishnan, G.: Exploiting symmetry and transactions for partial order reduction of rule based specifications. In: Valmari, A. (ed.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol.\u00a03925. Springer, Heidelberg (2006)"},{"key":"21_CR12","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of Parameterized Verification","author":"R. Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool, San Rafael (2015)"},{"key":"21_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large (extended abstract). In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02725, pp.\u00a0223\u2013235. Springer, Heidelberg (2003)"},{"key":"21_CR14","series-title":"LNCS","first-page":"561","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"B. Boigelot","year":"2004","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02988, pp.\u00a0561\u2013575. Springer, Heidelberg (2004)"},{"issue":"2","key":"21_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-011-0205-y","volume":"14","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 167\u2013191 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03114, pp.\u00a0372\u2013386. Springer, Heidelberg (2004)"},{"key":"21_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/3-540-45657-0_46","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Bouajjani","year":"2002","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404, pp.\u00a0539\u2013554. Springer, Heidelberg (2002)"},{"issue":"1","key":"21_CR18","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M. Browne","year":"1989","unstructured":"Browne, M., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"21_CR19","volume-title":"High Level Design Validation and Test Workshop (HLDVT)","author":"X. Chen","year":"2007","unstructured":"Chen, X., Yang, Y., DeLisi, M., Gopalakrishnan, G., Chou, C.T.: Hierarchical cache coherence protocol verification one level at a time through assume guarantee. In: High Level Design Validation and Test Workshop (HLDVT). IEEE, Piscataway (2007)"},{"key":"21_CR20","series-title":"LNCS","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"C.T. Chou","year":"2004","unstructured":"Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol.\u00a03312. Springer, Heidelberg (2004)"},{"issue":"5","key":"21_CR21","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. ACM Trans. Program. Lang. Syst. 19(5), 726\u2013750 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1\/2","key":"21_CR22","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1\/2), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"E.M. Clarke","year":"2006","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a03855, pp.\u00a0126\u2013141. Springer, Heidelberg (2006)"},{"key":"21_CR24","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633. Springer, Heidelberg (1999)"},{"key":"21_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a053\u201368. Springer, Heidelberg (2000)"},{"key":"21_CR26","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-0-387-35533-7_11","volume-title":"Formal Methods for Distributed System Development (FORTE)","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Verification of consistency protocols via infinite-state symbolic model checking. In: Bolognesi, T., Latella, D. (eds.) Formal Methods for Distributed System Development (FORTE), pp.\u00a0171\u2013186. Springer, Heidelberg (2000)"},{"key":"21_CR27","series-title":"LNCS","first-page":"313","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"G. Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a06269, pp.\u00a0313\u2013327. Springer, Heidelberg (2010)"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L.E. Dickson","year":"1913","unstructured":"Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n$n$ distinct prime factors. Am. J. Math. 35, 413\u2013422 (1913)","journal-title":"Am. J. Math."},{"key":"21_CR29","series-title":"LNCS","first-page":"236","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a01831, pp.\u00a0236\u2013254. Springer, Heidelberg (2000)"},{"key":"21_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","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.) Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a02860, pp.\u00a0247\u2013262. Springer, Heidelberg (2003)"},{"key":"21_CR31","first-page":"361","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0361\u2013370. IEEE, Piscataway (2003)"},{"key":"21_CR32","series-title":"LNCS","first-page":"144","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Rapid parameterized model checking of snoopy cache coherence protocols. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a0144\u2013159. Springer, Heidelberg (2003)"},{"key":"21_CR33","first-page":"85","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"E.A. Emerson","year":"1995","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Cytron, R.K., Lee, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a085\u201394. ACM, New York (1995)"},{"key":"21_CR34","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01102, pp.\u00a087\u201398. Springer, Heidelberg (1996)"},{"issue":"1\/2","key":"21_CR35","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1\/2), 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR36","first-page":"352","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0352\u2013359. IEEE, Piscataway (1999)"},{"issue":"1\u20132","key":"21_CR37","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! Theor. Comput. Syst. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Syst."},{"issue":"3","key":"21_CR38","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"21_CR39","series-title":"LNCS","first-page":"89","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01019, pp.\u00a089\u2013110. Springer, Heidelberg (1995)"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3) 2(7) (1952)","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"21_CR41","first-page":"97","volume-title":"Proc. Conf. on Computer Hardware Description Languages and Their Applications","author":"C.N. Ip","year":"1993","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Proc. Conf. on Computer Hardware Description Languages and Their Applications, pp.\u00a097\u2013111 (1993)"},{"issue":"1\/2","key":"21_CR42","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"21_CR43","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR44","series-title":"LNCS","first-page":"183","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Kelb","year":"1997","unstructured":"Kelb, P., Margaria, T., Mendler, M., Gsottberger, C.: Mosel: a flexible toolset for monadic second-order logic. In: Brinksma, E. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01217, pp.\u00a0183\u2013202. Springer, Heidelberg (1997)"},{"key":"21_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-63166-6_41","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a0424\u2013435. Springer, Heidelberg (1997)"},{"key":"21_CR46","volume-title":"Automated Verification of Infinite State Systems","author":"S. Krstic","year":"2005","unstructured":"Krstic, S.: Parameterized system verification with guard strengthening and parameter abstraction. In: Automated Verification of Infinite State Systems (2005)"},{"key":"21_CR47","first-page":"239","volume-title":"ACM Symp. on Principles of Distributed Computing (PODC)","author":"R.P. Kurshan","year":"1989","unstructured":"Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Rudnicki, P. (ed.) ACM Symp. on Principles of Distributed Computing (PODC), pp.\u00a0239\u2013247. ACM, New York (1989)"},{"key":"21_CR48","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a03114, pp.\u00a0135\u2013147. Springer, Heidelberg (2004)"},{"issue":"8","key":"21_CR49","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"21_CR50","first-page":"101","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"D. Lesens","year":"1996","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parametrized linear networks of processes. In: Boehm, H.-J., Steele, G.L. Jr. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0101\u2013105. ACM, New York (1996)"},{"key":"21_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-44585-4_29","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Maidl","year":"2001","unstructured":"Maidl, M.: A unifying model checking approach for safety properties of parameterized systems. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0311\u2013323. Springer, Heidelberg (2001)"},{"key":"21_CR52","series-title":"LNCS","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"21_CR53","series-title":"LNCS","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a01703. Springer, Heidelberg (1999)"},{"key":"21_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"K.L. McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a02144, pp.\u00a0179\u2013195. Springer, Heidelberg (2001)"},{"key":"21_CR55","volume-title":"IEEE Transactions on Software Engineering","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. In: IEEE Transactions on Software Engineering, vol.\u00a0SE-7. IEEE, Piscataway (1981)"},{"key":"21_CR56","series-title":"Formal Methods in Computer Aided Design (FMCAD)","volume-title":"Protocol Verification using Flows: Parameterized Verification using Message Flows","author":"J. O\u2019Leary","year":"2009","unstructured":"O\u2019Leary, J., Talupur, M., Tuttle, M.R.: Protocol Verification using Flows: Parameterized Verification using Message Flows. Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2009)"},{"key":"21_CR57","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/237502.237573","volume-title":"SPAA \u201996: Proceedings of the Eighth Annual ACM Symposium on Parallel Algorithms and Architectures","author":"S. Park","year":"1996","unstructured":"Park, S., Dill, D.L.: Verification of flash cache coherence protocol by aggregation of distributed transactions. In: SPAA \u201996: Proceedings of the Eighth Annual ACM Symposium on Parallel Algorithms and Architectures, pp.\u00a0288\u2013296. ACM, New York (1996)"},{"key":"21_CR58","series-title":"LNCS","first-page":"82","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a082\u201397. Springer, Heidelberg (2001)"},{"key":"21_CR59","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1,\u221e$0, 1, \\infty$)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02402, pp.\u00a0107\u2013122. Springer, Heidelberg (2002)"},{"key":"21_CR60","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-44585-4_4","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"A. Roychoudhury","year":"2001","unstructured":"Roychoudhury, A., Ramakrishnan, I.V.: Automated inductive verification of parameterized protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a025\u201337. Springer, Heidelberg (2001)"},{"key":"21_CR61","series-title":"LNCS","volume-title":"Intl. Symposium on Model Checking of Software (SPIN)","author":"D. Sethi","year":"2012","unstructured":"Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized model checking of fine grained concurrency. In: Donaldson, A.F., Parker, D. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol.\u00a07385. Springer, Heidelberg (2012)"},{"key":"21_CR62","series-title":"LNCS","first-page":"151","volume-title":"Workshop on Automatic Verification Methods for Finite State Systems","author":"Z. Shtadler","year":"1989","unstructured":"Shtadler, Z., Grumberg, O.: Network grammars, communication behaviors and automatic verification. In: Sifakis, J. (ed.) Workshop on Automatic Verification Methods for Finite State Systems. LNCS, pp.\u00a0151\u2013166. Springer, Heidelberg (1989)"},{"key":"21_CR63","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/s001650050040","volume":"11","author":"A.P. Sistla","year":"1999","unstructured":"Sistla, A.P., Gyuris, V.: Parameterized verification of linear networks using automata as invariants. Form. Asp. Comput. 11, 402\u2013425 (1999)","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"21_CR64","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I. Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"key":"21_CR65","first-page":"621","volume-title":"International Conference on Supercomputing (ICS)","author":"B.K. Szymanski","year":"1988","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Lenfant, J. (ed.) International Conference on Supercomputing (ICS), pp.\u00a0621\u2013626. ACM, New York (1988)"},{"key":"21_CR66","volume-title":"Proc. Workshop on Design of Correct Circuits (DCC)","author":"M. Talupur","year":"2008","unstructured":"Talupur, M., Krstic, S., O\u2019Leary, J., Tuttle, M.R.: Parametric verification of industrial strength cache coherence protocols. In: Proc. Workshop on Design of Correct Circuits (DCC) (2008)"},{"key":"21_CR67","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M. Talupur","year":"2008","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD). IEEE, Piscataway (2008)"},{"key":"21_CR68","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11691617_18","volume-title":"Intl. Symposium on Model Checking of Software (SPIN)","author":"C. Topnik","year":"2006","unstructured":"Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: a stand-alone tool and jABC plugin for M2L(Str). In: Valmari, A. (ed.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol.\u00a03925, pp.\u00a0293\u2013298. Springer, Heidelberg (2006)"},{"issue":"4","key":"21_CR69","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1016\/S1571-0661(04)00187-2","volume":"50","author":"T. Touili","year":"2001","unstructured":"Touili, T.: Regular model checking using widening techniques. Electron. Notes Theor. Comput. Sci. 50(4), 342\u2013356 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR70","first-page":"68","volume-title":"Workshop on Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Workshop on Automatic Verification Methods for Finite State Systems, pp.\u00a068\u201381. Springer, Heidelberg (1989)"},{"issue":"3\u20134","key":"21_CR71","first-page":"139","volume":"30","author":"L.D. Zuck","year":"2004","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3\u20134), 139\u2013169 (2004)","journal-title":"Comput. Lang. Syst. Struct."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T17:58:29Z","timestamp":1661277509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_21","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}