{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:55:18Z","timestamp":1743008118140,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026515"},{"type":"electronic","value":"9783642026522"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02652-2_12","type":"book-chapter","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T07:43:06Z","timestamp":1245915786000},"page":"125-142","source":"Crossref","is-referenced-by-count":9,"title":["A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks"],"prefix":"10.1007","author":[{"given":"Nicholas","family":"Kidd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-78800-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lal","year":"2008","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 282\u2013298. Springer, Heidelberg (2008)"},{"key":"12_CR3","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.: 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":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL (2003)","DOI":"10.1145\/604131.604137"},{"key":"12_CR5","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., 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":"12_CR6","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":"12_CR7","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL (2007)","DOI":"10.1145\/1190216.1190262"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Vaziri, M., Tip, F., Dolby, J.: Associating synchronization constraints with data in an object-oriented language. In: POPL (2006)","DOI":"10.1145\/1111037.1111067"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI (2003)","DOI":"10.1145\/781167.781169"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-93900-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Kidd","year":"2009","unstructured":"Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 198\u2013213. Springer, Heidelberg (2009)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci., vol.\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Kidd, N., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks. Technical Report 1649r, Univ.\u00a0of Wisconsin (April 2009), \n                    \n                      http:\/\/www.cs.wisc.edu\/wpis\/abstracts\/tr1649.abs.html","DOI":"10.1007\/978-3-642-02652-2_12"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-69166-2_19","volume-title":"Static Analysis","author":"N. Kidd","year":"2008","unstructured":"Kidd, N., Lal, A., Reps, T.: Language strength reduction. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 283\u2013298. Springer, Heidelberg (2008)"},{"key":"12_CR15","unstructured":"Kahlon, V., Gupta, A.: Personal communication (January 2009)"},{"key":"12_CR16","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TUM (2002)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Eytani, Y., Havelund, K., Stoller, S.D., Ur, S.: Towards a framework and a benchmark for testing tools for multi-threaded programs. Conc. and Comp. Prac. and Exp. 19(3) (2007)","DOI":"10.1002\/cpe.1068"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Reps, T.: Program analysis via graph reachability. Inf. and Softw. Tech.\u00a040 (1998)","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"12_CR19","volume-title":"Introduction to Formal Language Theory","author":"M. Harrison","year":"1978","unstructured":"Harrison, M.: Introduction to Formal Language Theory. Addison-Wesley, Reading (1978)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP\u00a058 (2005)","DOI":"10.21236\/ADA449102"},{"key":"12_CR21","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (February 2009), \n                    \n                      http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download.php"},{"key":"12_CR22","unstructured":"BuDDy: A BDD package (July 2004), \n                    \n                      http:\/\/buddy.wiki.sourceforge.net\/"},{"key":"12_CR23","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":"12_CR24","doi-asserted-by":"crossref","unstructured":"Lammich, P., M\u00fcller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: CAV (2009) (to appear)","DOI":"10.1007\/978-3-642-02658-4_39"}],"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-642-02652-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:06:02Z","timestamp":1558267562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02652-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026515","9783642026522"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02652-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}