{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:22Z","timestamp":1760202562250},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851134"},{"type":"electronic","value":"9783540851141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_19","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T23:22:48Z","timestamp":1218583368000},"page":"270-287","source":"Crossref","is-referenced-by-count":33,"title":["Symbolic Context-Bounded Analysis of Multithreaded Java Programs"],"prefix":"10.1007","author":[{"given":"Dejvuth","family":"Suwimonteerabuth","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronisation-sensitive analysis is undecidable. ACM Trans. Programming Languages and Systems\u00a022, 416\u2013430 (2000)","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"},{"key":"19_CR4","first-page":"303","volume-title":"Proc. POPL","author":"V. Kahlon","year":"2007","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: Proc. POPL, pp. 303\u2013314. ACM, New York (2007)"},{"key":"19_CR5","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/964001.964022","volume-title":"Proc. POPL","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: Proc. POPL, pp. 245\u2013255. ACM, New York (2004)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/11817963_29","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 300\u2013314. Springer, Heidelberg (2006)"},{"key":"19_CR7","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1145\/604131.604137","volume-title":"Proc. POPL","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proc. POPL, pp. 62\u201373. ACM Press, New York (2003)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: Reachability analysis of synchronized PA-systems. In: Proc. Infinity (2004)","DOI":"10.1016\/j.entcs.2005.02.063"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E.M., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-540-73368-3_28","volume-title":"Computer Aided Verification","author":"G. Patin","year":"2007","unstructured":"Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of multithreaded dynamic and recursive programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 254\u2013257. Springer, Heidelberg (2007)"},{"key":"19_CR11","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":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11590156_28","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strej\u010dek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhudusan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Proc. TACAS. LNCS, vol.\u00a04963, pp. 299\u2013314 (2008)","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Proc. TACAS. LNCS, vol.\u00a04963, pp. 282\u2013298 (2008)","DOI":"10.1007\/978-3-540-78800-3_20"},{"key":"19_CR15","unstructured":"jMoped: The tool\u2019s website, http:\/\/www7.in.tum.de\/tools\/jmoped\/"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-73368-3_19","volume-title":"Computer Aided Verification","author":"D. Suwimonteerabuth","year":"2007","unstructured":"Suwimonteerabuth, D., Berger, F., Schwoon, S., Esparza, J.: jMoped: A test environment for Java programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 164\u2013167. Springer, Heidelberg (2007)"},{"issue":"2","key":"19_CR19","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.\u00a032(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Software Eng."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14\u201324 (2004)","DOI":"10.1145\/996841.996845"},{"issue":"3","key":"19_CR21","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1145\/320613.320619","volume":"5","author":"H.T. Kung","year":"1980","unstructured":"Kung, H.T., Lehman, P.L.: Concurrent manipulation of binary search trees. ACM Trans. Database Syst.\u00a05(3), 354\u2013382 (1980)","journal-title":"ACM Trans. Database Syst."},{"issue":"4","key":"19_CR22","first-page":"401","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE TCAD\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE TCAD"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T11:15:51Z","timestamp":1684494951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}