{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:04:50Z","timestamp":1767773090670,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_22","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"299-313","source":"Crossref","is-referenced-by-count":36,"title":["Symmetry and Completeness in the Analysis of Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., et al.: Handling global conditions in parameterized system verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"issue":"6","key":"22_CR2","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.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., et al.: Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore\u00a0D. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/11513988_39","volume-title":"Computer Aided Verification","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., et al.: IIV: An invisible nvariant verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 408\u2013412. Springer, Heidelberg (2005)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45420-9","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","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, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"issue":"1","key":"22_CR7","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput.\u00a081(1), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(4) (1981)","DOI":"10.1109\/TSE.1981.230844"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp. 294\u2013303 (1987)","DOI":"10.1145\/41840.41865"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 126\u2013141. Springer, Heidelberg (2005)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319628"},{"key":"22_CR12","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods","author":"W.-P. Roeve de","year":"2001","unstructured":"de Roeve, W-P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, Cambridge (2001)"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM 18(8) (1975)","DOI":"10.1145\/360933.360975"},{"key":"22_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, Springer, Heidelberg (2000)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems (extended abstract). In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 87\u201398. Springer, Heidelberg (1996)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: ACM Symposium on Principles of Programming Languages (1995)","DOI":"10.1145\/199448.199468"},{"issue":"1-3","key":"22_CR18","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., et al.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/503272.503291"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"German, S., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM (1992)","DOI":"10.1145\/146637.146681"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., et al.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., et al.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"22_CR27","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems (TOPLAS) (1983)","DOI":"10.1145\/69575.69577"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1) (2000)","DOI":"10.1006\/inco.2000.3000"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., et al.: Symbolic model checking with rich ssertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"issue":"4","key":"22_CR31","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. STTT\u00a02(4), 328\u2013342 (2000)","journal-title":"STTT"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: PODC, pp. 239\u2013247 (1989)","DOI":"10.1145\/72981.72998"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-540-24622-0_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 267\u2013281. Springer, Heidelberg (2004)"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Computer Aided Verification","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.) CAV 2004. LNCS, vol.\u00a03114, pp. 135\u2013147. Springer, Heidelberg (2004)"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2) (1977)","DOI":"10.1109\/TSE.1977.229904"},{"key":"22_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Lazic","year":"2000","unstructured":"Lazic, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 581\u2013595. Springer, Heidelberg (2000)"},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"issue":"5","key":"22_CR38","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"22_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"22_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996)"},{"key":"22_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_2","volume-title":"CONCUR 2002 - Concurrency Theory","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"issue":"4","key":"22_CR42","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.\u00a028(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"key":"22_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:07Z","timestamp":1620017107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_22","relation":{},"subject":[]}}