{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T21:20:30Z","timestamp":1769721630787,"version":"3.49.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2011,4,7]],"date-time":"2011-04-07T00:00:00Z","timestamp":1302134400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2011,12]]},"DOI":"10.1007\/s10515-011-0085-0","type":"journal-article","created":{"date-parts":[[2011,4,7]],"date-time":"2011-04-07T05:27:45Z","timestamp":1302154065000},"page":"325-362","source":"Crossref","is-referenced-by-count":7,"title":["Symbolic modular deadlock analysis"],"prefix":"10.1007","volume":"18","author":[{"given":"Jyotirmoy V.","family":"Deshmukh","sequence":"first","affiliation":[]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,4,7]]},"reference":[{"key":"85_CR1","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/1147403.1147413","volume-title":"Proc. of Workshop on Parallel and Distributed Systems: Testing and Debugging","author":"R. Agarwal","year":"2006","unstructured":"Agarwal, R., Stoller, S.D.: Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables. In: Proc. of Workshop on Parallel and Distributed Systems: Testing and Debugging, pp.\u00a051\u201360 (2006)"},{"key":"85_CR2","first-page":"191","volume-title":"Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring. Hardware and Software, Verification and Testing","author":"R. Agarwal","year":"2006","unstructured":"Agarwal, R., Wang, L., Stoller, S.: Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring. Hardware and Software, Verification and Testing, pp.\u00a0191\u2013207 (2006)"},{"key":"85_CR3","unstructured":"Open Source Mail Archive (2004) Message #150. URL http:\/\/osdir.com\/ml\/java.hsqldb.user\/2004-03\/msg00150.html"},{"key":"85_CR4","unstructured":"Open Source Mail Archive (2008) Bug 159. URL http:\/\/osdir.com\/ml\/java.openjdk.distro-packaging.devel\/2008-06\/msg00061.html"},{"key":"85_CR5","first-page":"68","volume-title":"Proc. of the 13th Australian Conference on Software Engineering","author":"C. Artho","year":"2001","unstructured":"Artho, C., Biere, A.: Applying static analysis to large-scale, multi-threaded Java programs. In: Proc. of the 13th Australian Conference on Software Engineering, p.\u00a068 (2001)"},{"key":"85_CR6","first-page":"208","volume-title":"Proc. of the Haifa Verification Conference","author":"S. Bensalem","year":"2005","unstructured":"Bensalem, S., Havelund, K.: Dynamic deadlock analysis of multi-threaded programs. In: Proc. of the Haifa Verification Conference, pp.\u00a0208\u2013223 (2005)"},{"key":"85_CR7","first-page":"52","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, pp.\u00a052\u201371 (1981)"},{"issue":"3","key":"85_CR8","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/32.489078","volume":"22","author":"J.C. Corbett","year":"1996","unstructured":"Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. IEEE Trans. Softw. Eng. 22(3), 161\u2013180 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"85_CR9","unstructured":"Sun Developer Network Bug Database (2007). URL http:\/\/bugs.sun.com\/bugdatabase\/view_bug.do?bug_id=xxxx , bug-id provided at citation"},{"key":"85_CR10","first-page":"480","volume-title":"Proc. of the 24th IEEE \/ACM International Conference on Automated Software Engineering","author":"J.V. Deshmukh","year":"2009","unstructured":"Deshmukh, J.V., Emerson, E.A., Sankaranarayanan, S.: Symbolic deadlock analysis in concurrent libraries and their clients. In: Proc. of the 24th IEEE \/ACM International Conference on Automated Software Engineering, pp.\u00a0480\u2013491 (2009)"},{"key":"85_CR11","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Proc. of Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proc. of Computer Aided Verification, pp.\u00a081\u201394 (2006)"},{"issue":"5","key":"85_CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/1165389.945468","volume":"37","author":"D. Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. ACM SIGOPS Oper. Syst. Rev. 37(5), 237\u2013252 (2003)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"85_CR13","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/1375581.1375618","volume-title":"Proc. of PLDI","author":"C. Flanagan","year":"2008","unstructured":"Flanagan, C., Freund, S.N., Yi, J.: Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: Proc. of PLDI, pp.\u00a0293\u2013303 (2008)"},{"key":"85_CR14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"Proc. of SPIN Workshop on Model Checking of Software","author":"K. Havelund","year":"2000","unstructured":"Havelund, K.: Using runtime analysis to guide model checking of Java programs. In: Proc. of SPIN Workshop on Model Checking of Software, pp.\u00a0245\u2013264 (2000)"},{"issue":"4","key":"85_CR15","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using Java pathfinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"85_CR16","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"85_CR17","unstructured":"Jajuk Advanced Jukebox (2008). Bug Ticket #850. URL http:\/\/trac.jajuk.info\/ticket\/850"},{"key":"85_CR18","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/11559306_9","volume-title":"Proc. of Frontiers of Combining Systems, 5th International Workshop","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proc. of Frontiers of Combining Systems, 5th International Workshop, pp.\u00a0168\u2013183 (2005)"},{"issue":"7","key":"85_CR19","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). URL http:\/\/portal.acm.org.ezproxy.lib.utexas.edu\/citation.cfm?id=359563","journal-title":"Commun. ACM"},{"key":"85_CR20","first-page":"194","volume-title":"Proc. of the 17th International Workshop on Languages and Compilers for Parallel Computing","author":"L. Li","year":"2004","unstructured":"Li, L., Verbrugge, C.: A practical MHP information analysis for concurrent Java programs. In: Proc. of the 17th International Workshop on Languages and Compilers for Parallel Computing, pp.\u00a0194\u2013208 (2004)"},{"issue":"3","key":"85_CR21","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/850644.850645","volume":"11","author":"A. Lister","year":"1977","unstructured":"Lister, A.: The problem of nested monitor calls. SIGOPS Oper. Syst. Rev. 11(3), 5\u20137 (1977)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"85_CR22","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Proc. of Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proc. of Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0337\u2013340 (2008)"},{"key":"85_CR23","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1145\/1133981.1134018","volume-title":"Proc. of the 2006 ACM SIGPLAN Conf. on Programming Language Design and Implementation","author":"M. Naik","year":"2006","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for Java. In: Proc. of the 2006 ACM SIGPLAN Conf. on Programming Language Design and Implementation, pp.\u00a0308\u2013319. ACM, New York (2006)"},{"key":"85_CR24","first-page":"386","volume-title":"Proc. of the 31st International Conference on Software Engineering","author":"M. Naik","year":"2009","unstructured":"Naik, M., Park, C.S., Sen, K., Gay, D.: Effective static deadlock detection. In: Proc. of the 31st International Conference on Software Engineering, pp.\u00a0386\u2013396 (2009)"},{"key":"85_CR25","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1145\/1370082.1370093","volume-title":"Proc. of 1st International Workshop on Multicore Software Engineering","author":"F. Otto","year":"2008","unstructured":"Otto, F., Moschny, T.: Finding synchronization defects in Java programs: extended static analyses and code patterns. In: Proc. of 1st International Workshop on Multicore Software Engineering, pp.\u00a041\u201346 (2008)"},{"key":"85_CR26","doi-asserted-by":"crossref","unstructured":"von Praun, C.: Detecting synchronization defects in multi-threaded object-oriented programs. PhD thesis, ETH Zurich (2004)","DOI":"10.1145\/780822.781145"},{"issue":"2","key":"85_CR27","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. Program. Lang. Syst. 22(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"85_CR28","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1109\/APSEC.2008.68","volume-title":"Proc. of the 15th Asia-Pacific Software Engineering Conference","author":"V.K. Shanbhag","year":"2008","unstructured":"Shanbhag, V.K.: Deadlock-detection in Java-library using static-analysis. In: Proc. of the 15th Asia-Pacific Software Engineering Conference, pp.\u00a0361\u2013368 (2008)"},{"key":"85_CR29","first-page":"125","volume-title":"Proc. of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research","author":"R. Vall\u00e9e-Rai","year":"1999","unstructured":"Vall\u00e9e-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot\u2014a Java Optimization Framework. In: Proc. of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research, pp.\u00a0125\u2013135 (1999)"},{"key":"85_CR30","first-page":"602","volume-title":"Proc. of the European Conference on Object-Oriented Programming","author":"A. Williams","year":"2005","unstructured":"Williams, A., Thies, W., Ernst, M.D.: Static deadlock detection for Java libraries. In:Proc. of the European Conference on Object-Oriented Programming, pp.\u00a0602\u2013629 (2005)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-011-0085-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-011-0085-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-011-0085-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,9]],"date-time":"2019-06-09T20:12:23Z","timestamp":1560111143000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-011-0085-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,7]]},"references-count":30,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2011,12]]}},"alternative-id":["85"],"URL":"https:\/\/doi.org\/10.1007\/s10515-011-0085-0","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4,7]]}}}