{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T03:21:35Z","timestamp":1785295295948,"version":"3.55.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,5,21]],"date-time":"2010-05-21T00:00:00Z","timestamp":1274400000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1007\/s10009-010-0159-5","type":"journal-article","created":{"date-parts":[[2010,5,19]],"date-time":"2010-05-19T23:01:09Z","timestamp":1274310069000},"page":"37-60","source":"Crossref","is-referenced-by-count":6,"title":["A decision procedure for detecting atomicity violations for communicating processes with locks"],"prefix":"10.1007","volume":"13","author":[{"given":"Nicholas","family":"Kidd","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,5,21]]},"reference":[{"key":"159_CR1","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: CONCUR (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"159_CR2","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":"159_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: CONCUR (2005)","DOI":"10.1007\/11539452_36"},{"key":"159_CR4","unstructured":"BuDDy: A BDD package. http:\/\/buddy.wiki.sourceforge.net\/ (2004)"},{"key":"159_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: TACAS (2006)","DOI":"10.1007\/11691372_22"},{"issue":"3","key":"159_CR6","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1002\/cpe.1068","volume":"19","author":"Y. Eytani","year":"2007","unstructured":"Eytani Y., Havelund K., Stoller S.D., Ur S.: Towards a framework and a benchmark for testing tools for multi-threaded programs. Conc. Comp. Prac. Exp. 19(3), 267\u2013279 (2007)","journal-title":"Conc. Comp. Prac. Exp."},{"key":"159_CR7","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S1571-0661(05)80426-8","volume":"9","author":"A. Finkel","year":"1997","unstructured":"Finkel A., Willems B., Wolper P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci 9, 27\u201337 (1997)","journal-title":"Electron. Notes Theor. Comput. Sci"},{"key":"159_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI (2003)","DOI":"10.1145\/781131.781169"},{"key":"159_CR9","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":"159_CR10","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":"159_CR11","unstructured":"Kahlon, V., Gupta, A.: Personal communication (2009)"},{"key":"159_CR12","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: CAV (2005)","DOI":"10.1007\/11513988_49"},{"key":"159_CR13","doi-asserted-by":"crossref","unstructured":"Kidd, N., Lal, A., Reps, T.: Language strength reduction. In: SAS (2008)","DOI":"10.1007\/978-3-540-69166-2_19"},{"key":"159_CR14","unstructured":"Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library. http:\/\/www.cs.wisc.edu\/wpis\/wpds\/download.php (2009)"},{"key":"159_CR15","doi-asserted-by":"crossref","unstructured":"Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: VMCAI (2009)","DOI":"10.1007\/978-3-540-93900-9_18"},{"key":"159_CR16","doi-asserted-by":"crossref","unstructured":"Kidd, N.A., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks. In: SPIN (2009)","DOI":"10.1007\/978-3-642-02652-2_12"},{"key":"159_CR17","doi-asserted-by":"crossref","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: TACAS (2008)","DOI":"10.1007\/978-3-540-78800-3_20"},{"key":"159_CR18","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)","DOI":"10.1007\/978-3-642-02658-4_39"},{"key":"159_CR19","doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes\u2014a comprehensive study on real world concurrency bug characteristics. In: ASPLOS (2008)","DOI":"10.1145\/1346281.1346323"},{"key":"159_CR20","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"159_CR21","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Programming. Lang. Syst. 22, 416\u2013430 (2000)","journal-title":"ACM Trans. Programming. Lang. Syst."},{"key":"159_CR22","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0950-5849(98)00093-7","volume":"40","author":"T. Reps","year":"1998","unstructured":"Reps T.: Program analysis via graph reachability. Inf. Softw. Technol. 40, 5\u201319 (1998)","journal-title":"Inf. Softw. Technol."},{"key":"159_CR23","first-page":"206","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. SCP 58, 206\u2013263 (2005)","journal-title":"SCP"},{"key":"159_CR24","unstructured":"Schwoon, S.: Model-checking pushdown systems. PhD thesis, TUM (2002)"},{"key":"159_CR25","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"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0159-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0159-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0159-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T05:22:24Z","timestamp":1559107344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0159-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,21]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["159"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0159-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5,21]]}}}