{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:44:49Z","timestamp":1725565489302},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_16","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"253-270","source":"Crossref","is-referenced-by-count":8,"title":["Compositional Bitvector Analysis for Concurrent Programs with Nested Locks"],"prefix":"10.1007","author":[{"given":"Azadeh","family":"Farzan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","volume-title":"Compilers: principles, techniques, and tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1986)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Chugh, R., Voung, J., Jhala, R., Lerner, S.: Dataflow analysis for concurrent programs using datarace detection. In: PLDI, pp. 316\u2013326 (2008)","DOI":"10.1145\/1375581.1375620"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL, pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional bitvector analysis for concurrent programs with nested locks.Technical report, University of Toronto (2010), http:\/\/www.cs.toronto.edu\/~zkincaid\/pub\/cbva.pdf","DOI":"10.1007\/978-3-642-15769-1_16"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL, pp. 303\u2013314 (2007)","DOI":"10.1145\/1190216.1190262"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, 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":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-02652-2_12","volume-title":"Model Checking Software","author":"N. Kidd","year":"2009","unstructured":"Kidd, N., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol.\u00a05578, pp. 125\u2013142. Springer, Heidelberg (2009)"},{"issue":"3","key":"16_CR9","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/229542.229545","volume":"18","author":"J. Knoop","year":"1996","unstructured":"Knoop, J., Steffen, B., Vollmer, J.: Parallelism for free: Efficient and optimal bitvector analyses for parallel programs. TOPLAS\u00a018(3), 268\u2013299 (1996)","journal-title":"TOPLAS"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/BFb0057887","volume-title":"Euro-Par\u201998 Parallel Processing","author":"J. Knoop","year":"1998","unstructured":"Knoop, J.: Parallel constant propagation. In: Pritchard, D., Reeve, J.S. (eds.) Euro-Par 1998. LNCS, vol.\u00a01470, pp. 445\u2013455. Springer, Heidelberg (1998)"},{"issue":"7","key":"16_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/277633.277638","volume":"33","author":"J. Krinke","year":"1998","unstructured":"Krinke, J.: Static slicing of threaded programs. SIGPLAN Not.\u00a033(7), 35\u201342 (1998)","journal-title":"SIGPLAN Not."},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-69166-2_14","volume-title":"Static Analysis","author":"P. Lammich","year":"2008","unstructured":"Lammich, P., M\u00fcller-Olm, M.: Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 205\u2013220. Springer, Heidelberg (2008)"},{"issue":"12","key":"16_CR13","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. ACM Commun.\u00a018(12), 717\u2013721 (1975)","journal-title":"ACM Commun."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Masticola, S.P., Ryder, B.G.: Non-concurrency analysis. In: PPOPP, New York, NY, USA, pp. 129\u2013138 (1993)","DOI":"10.1145\/155332.155346"},{"key":"16_CR15","volume-title":"Advanced Compiler Design and Imlementation","author":"S.S. Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Imlementation. Morgan Kaufmann, San Francisco (1997)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Naumovich, G., Avrunin, G.S.: A conservative data flow algorithm for detecting all pairs of statements that happen in parallel. In: FSE, pp. 24\u201334 (1998)","DOI":"10.1145\/288195.288213"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Naumovich, G., Avrunin, G.S., Clarke, L.A.: An efficient algorithm for computing mhp information for concurrent java programs. In: ESEC\/FSE-7, pp. 338\u2013354 (1999)","DOI":"10.1007\/3-540-48166-4_21"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.: Type and effect systems. In: Correct System Design, pp. 114\u2013136 (1999)","DOI":"10.1007\/3-540-48092-7_6"},{"issue":"1-2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program.\u00a058(1-2), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program."},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: PPoPP (2001)","DOI":"10.1145\/379539.379553"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-46425-5_23","volume-title":"Programming Languages and Systems","author":"H. Seidl","year":"2000","unstructured":"Seidl, H., Steffen, B.: Constraint-based inter-procedural analysis of parallel programs. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 351\u2013365. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:40:17Z","timestamp":1606185617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}