{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:08:44Z","timestamp":1763467724865},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_9","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"126-141","source":"Crossref","is-referenced-by-count":53,"title":["Environment Abstraction for Parameterized Verification"],"prefix":"10.1007","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Muralidhar","family":"Talupur","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-45694-5_9","volume-title":"CONCUR 2002 - Concurrency Theory","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., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, p. 116. Springer, Heidelberg (2002)"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"Apt, K., Kozen, D.: Limits for automatic verification of finite state concurrent systems. Information Processing Letters\u00a015, 307\u2013309 (1986)","journal-title":"Information Processing Letters"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 221. Springer, Heidelberg (2001)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Chaki, S., Rajamani, S.: Verification of multi-threaded software libraries. In: ICSE (2001)","DOI":"10.1007\/3-540-45319-9_12"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46419-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Baukus","year":"2000","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S systems to verify parameterized networks. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 188. Springer, Heidelberg (2000)"},{"key":"9_CR6","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Verification of parameterized protocols. Journal of Universal of Computer Science (2001)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"9_CR9","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. Information and Computation\u00a081, 13\u201331 (1989)","journal-title":"Information and Computation"},{"key":"9_CR10","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification, http:\/\/www.cs.cmu.edu\/~tmurali\/vmcai06.ps"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0028174","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1993","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automated verification of cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, A.E., Kahlon, V.: Model checking guarded protocols. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 361\u2013370 (2003)","DOI":"10.1109\/LICS.2003.1210076"},{"key":"9_CR14","unstructured":"Emerson, E.A., Havlicek, J., Trefler, R.: Virtual symmetry. In: 15th Annual IEEE Symposium on Logic in Computer Science, LICS (2000)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.: Utilizing symmetry when model-checking under fairness assumptions: An automata theoretic approach. TOPLAS\u00a04 (1997)","DOI":"10.1145\/262004.262008"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48153-2_12","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Trefler, R.: From asymmetry to full symmetry. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 142\u2013157. Springer, Heidelberg (1999)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-24622-0_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with incomprehensible ranking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 223\u2013238. Springer, Heidelberg (2004)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-24730-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Fang","year":"2004","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.: Liveness with invisible ranking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 482\u2013496. Springer, Heidelberg (2004)"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM\u00a039 (1992)","DOI":"10.1145\/146637.146681"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R.: Race checking with context inference. In: Proceedings of the International Conference on Programming Language Design and Implementation, PLDI (2004)","DOI":"10.1145\/996841.996844"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","first-page":"424","volume-title":"Computer Aided Verification","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.) CAV 1997. LNCS, vol.\u00a01254, pp. 424\u2013435. Springer, Heidelberg (1997)"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.: Constructing quantified invariants. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988. Springer, Heidelberg (2004)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: 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)"},{"issue":"8","key":"9_CR26","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. Communications of the ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Communications of the ACM"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/10722167_25","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 312\u2013327. Springer, Heidelberg (2000)"},{"key":"9_CR28","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.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 82. Springer, Heidelberg (2001)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1,\u2009\u221e\u2009) counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 107. Springer, Heidelberg (2002)"},{"key":"9_CR30","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. Information Processing Letters\u00a028, 213\u2013214 (1988)","journal-title":"Information Processing Letters"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Proc International Conference on Supercomputing Systems (1988)","DOI":"10.1145\/55364.55425"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:07Z","timestamp":1619507227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11609773_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}