{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:11:40Z","timestamp":1774987900586,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_54","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"629-644","source":"Crossref","is-referenced-by-count":52,"title":["Model-Checking Parameterized Concurrent Programs Using Linear Interfaces"],"prefix":"10.1007","author":[{"given":"Salvatore","family":"La Torre","sequence":"first","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"54_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"TACAS","author":"M.F. Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: TACAS. LNCS, vol.\u00a05505, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"54_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"CAV 2009","author":"G. Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 64\u201378. Springer, Heidelberg (2009)"},{"key":"54_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume-title":"CONCUR \u201995 Concurrency Theory","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Veryfying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 395\u2013407. Springer, Heidelberg (1995)"},{"key":"54_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"54_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for linear-time properties of concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"key":"54_CR6","unstructured":"Creese, S.J., Roscoe, A.W.: Data independent induction over structured networks. In: PDPTA.CSREA Press (2000)"},{"key":"54_CR7","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)"},{"key":"54_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-56922-7_38","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, pp. 463\u2013478. Springer, Heidelberg (1993)"},{"key":"54_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-02138-1_4","volume-title":"Formal Techniques for Distributed Systems","author":"N. Ghafari","year":"2009","unstructured":"Ghafari, N., Gurfinkel, A., Trefler, R.J.: Verification of parameterized systems with combinations of abstract domains. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol.\u00a05522, pp. 57\u201372. Springer, Heidelberg (2009)"},{"issue":"3","key":"54_CR10","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C.N. Ip","year":"1999","unstructured":"Ip, C.N., Dill, D.L.: Verifying systems with replicated components in murphi. Formal Methods in System Design\u00a014(3), 273\u2013310 (1999)","journal-title":"Formal Methods in System Design"},{"key":"54_CR11","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":"54_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"key":"54_CR13","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/1542476.1542500","volume-title":"PLDI","author":"S. Torre La","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: PLDI, pp. 211\u2013222. ACM, New York (2009)"},{"key":"54_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"CAV 2009","author":"S. Torre La","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 477\u2013492. Springer, Heidelberg (2009)"},{"key":"54_CR15","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking Parameterized Concurrent Programs using Linear Interfaces IDEALS Technical Report, University of Illinois, \n                    \n                      http:\/\/hdl.handle.net\/2142\/15410"},{"key":"54_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Log.\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297662"},{"key":"54_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"54_CR18","first-page":"446","volume-title":"PLDI","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446\u2013455. ACM, New York (2007)"},{"key":"54_CR19","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.D.: Liveness with (0, 1, \u221e)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"54_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"54_CR21","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/996841.996845","volume-title":"PLDI","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI, pp. 14\u201324. ACM, New York (2004)"},{"key":"54_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-85114-1_19","volume-title":"Model Checking Software","author":"D. Suwimonteerabuth","year":"2008","unstructured":"Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic context-bounded analysis of multithreaded java programs. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 270\u2013287. Springer, Heidelberg (2008)"},{"key":"54_CR23","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/1321631.1321719","volume-title":"ASE","author":"T. Witkowski","year":"2007","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: ASE, pp. 501\u2013504. ACM, New York (2007)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:23:38Z","timestamp":1619785418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}