{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T18:51:51Z","timestamp":1773773511043,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,8,25]],"date-time":"2016-08-25T00:00:00Z","timestamp":1472083200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,8,25]]},"DOI":"10.1145\/2970276.2970309","type":"proceedings-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T12:40:09Z","timestamp":1472215209000},"page":"379-390","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Sound static deadlock analysis for C\/Pthreads"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Kroening","sequence":"first","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Daniel","family":"Poetzl","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[{"name":"University of Sussex, UK"}]},{"given":"Bj\u00f6rn","family":"Wachter","sequence":"additional","affiliation":[{"name":"SSW-Trading, Germany"}]}],"member":"320","published-online":{"date-parts":[[2016,8,25]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1147\/JRD.2010.2060276"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147403.1147413"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_3"},{"key":"e_1_3_2_1_4_1","first-page":"75","volume-title":"Australian Software Engineering Conference","author":"Artho C.","unstructured":"C. Artho and A. Biere . Applying static analysis to large-scale, multi-threaded Java programs . In Australian Software Engineering Conference , pages 68\u2013 75 . IEEE, 2001. C. Artho and A. Biere. Applying static analysis to large-scale, multi-threaded Java programs. In Australian Software Engineering Conference, pages 68\u201375. IEEE, 2001."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_45"},{"key":"e_1_3_2_1_6_1","first-page":"129","volume-title":"Formal Methods and Models for Codesign","author":"Bensalem S.","unstructured":"S. Bensalem , A. Griesmayer , A. Legay , T. Nguyen , and D. Peled . Efficient deadlock detection for concurrent systems . In Formal Methods and Models for Codesign , pages 119\u2013 129 . IEEE, 2011. S. Bensalem, A. Griesmayer, A. Legay, T. Nguyen, and D. Peled. Efficient deadlock detection for concurrent systems. In Formal Methods and Models for Codesign, pages 119\u2013129. IEEE, 2011."},{"key":"e_1_3_2_1_7_1","first-page":"234","volume":"892","author":"Burke M. G.","year":"1995","unstructured":"M. G. Burke , P. R. Carini , J.-D. Choi , and M. Hind . Flow-insensitive interprocedural alias analysis in the presence of pointers. In LCPC , volume 892 of LNCS, pages 234 \u2013 250 . Springer, 1995 . M. G. Burke, P. R. Carini, J.-D. Choi, and M. Hind. Flow-insensitive interprocedural alias analysis in the presence of pointers. In LCPC, volume 892 of LNCS, pages 234\u2013250. Springer, 1995.","journal-title":"In LCPC"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2301725"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2012.40"},{"key":"e_1_3_2_1_10_1","first-page":"168","volume":"2988","author":"Clarke E. M.","year":"2004","unstructured":"E. M. Clarke , D. Kroening , and F. Lerda . A tool for checking ANSI-C programs. In TACAS , volume 2988 of LNCS, pages 168 \u2013 176 . Springer, 2004 . E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, volume 2988 of LNCS, pages 168\u2013176. Springer, 2004.","journal-title":"A tool for checking ANSI-C programs. In TACAS"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635918"},{"key":"e_1_3_2_1_15_1","volume-title":"Knowledge Systems Institute Graduate School","author":"Feldt R.","year":"2010","unstructured":"R. Feldt and A. Magazinius . Validity threats in empirical software engineering research \u2013 an initial survey. In Software Engineering & Knowledge Engineering (SEKE), pages 374\u2013379 . Knowledge Systems Institute Graduate School , 2010 . R. Feldt and A. Magazinius. Validity threats in empirical software engineering research \u2013 an initial survey. In Software Engineering & Knowledge Engineering (SEKE), pages 374\u2013379. Knowledge Systems Institute Graduate School, 2010."},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","first-page":"288","volume-title":"FMOODS\/FORTE","author":"Flores-Montoya A.","unstructured":"A. Flores-Montoya , E. Albert , and S. Genaim . May-happen-in-parallel based deadlock analysis for concurrent objects . In FMOODS\/FORTE , volume 7892 of LNCS , pages 273\u2013 288 . Springer, 2013. A. Flores-Montoya, E. Albert, and S. Genaim. May-happen-in-parallel based deadlock analysis for concurrent objects. In FMOODS\/FORTE, volume 7892 of LNCS, pages 273\u2013288. Springer, 2013."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_19"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"264","volume-title":"SPIN","author":"Havelund K.","unstructured":"K. Havelund . Using runtime analysis to guide model checking of Java programs . In SPIN , volume 1885 of LNCS , pages 245\u2013 264 . Springer, 2000. K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN, volume 1885 of LNCS, pages 245\u2013264. Springer, 2000."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_20_1","volume-title":"C standard","author":"International Organization for Standardization.","year":"2011","unstructured":"International Organization for Standardization. C standard , 2011 . ISO\/IEC 9899:2011. International Organization for Standardization. C standard, 2011. ISO\/IEC 9899:2011."},{"key":"e_1_3_2_1_21_1","first-page":"812","volume-title":"ASE","author":"Inverso O.","unstructured":"O. Inverso , T. L. Nguyen , B. Fischer , S. La Torre , and G. Parlato . Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs . In ASE , pages 807\u2013 812 . IEEE, 2015. O. Inverso, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. In ASE, pages 807\u2013812. IEEE, 2015."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882339"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542489"},{"key":"e_1_3_2_1_24_1","first-page":"239","volume-title":"CAV","author":"Kahlon V.","unstructured":"V. Kahlon , Y. Yang , S. Sankaranarayanan , and A. Gupta . Fast and accurate static data-race detection for concurrent programs . In CAV , pages 226\u2013 239 . Springer, 2007. V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta. Fast and accurate static data-race detection for concurrent programs. In CAV, pages 226\u2013239. Springer, 2007."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/277631.277638"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940096"},{"key":"e_1_3_2_1_27_1","volume-title":"Sound static deadlock analysis for C\/Pthreads (extended version). CoRR, abs\/1607.06927","author":"Kroening D.","year":"2016","unstructured":"D. Kroening , D. Poetzl , P. Schrammel , and B. Wachter . Sound static deadlock analysis for C\/Pthreads (extended version). CoRR, abs\/1607.06927 , 2016 . D. Kroening, D. Poetzl, P. Schrammel, and B. Wachter. Sound static deadlock analysis for C\/Pthreads (extended version). CoRR, abs\/1607.06927, 2016."},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"39","volume-title":"MEMICS","author":"Kroening D.","unstructured":"D. Kroening and M. Tautschnig . Automating software analysis at large scale . In MEMICS , volume 8934 of LNCS , pages 30\u2013 39 . Springer, 2014. D. Kroening and M. Tautschnig. Automating software analysis at large scale. In MEMICS, volume 8934 of LNCS, pages 30\u201339. Springer, 2014."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_4"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.22"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/155332.155346"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.349121"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288213"},{"key":"e_1_3_2_1_35_1","series-title":"LNCS","first-page":"19","volume-title":"SAS","author":"Rinard M. C.","unstructured":"M. C. Rinard . Analysis of multithreaded programs. In SAS , volume 2126 of LNCS , pages 1\u2013 19 . Springer, 2001. M. C. Rinard. Analysis of multithreaded programs. In SAS, volume 2126 of LNCS, pages 1\u201319. Springer, 2001."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_13"},{"key":"e_1_3_2_1_38_1","volume-title":"The open group base specifications issue 7","author":"The Open Group and IEEE.","year":"2013","unstructured":"The Open Group and IEEE. The open group base specifications issue 7 , 2013 . IEEE Std 1003.1-2008\/Cor 1-2013. The Open Group and IEEE. The open group base specifications issue 7, 2013. IEEE Std 1003.1-2008\/Cor 1-2013."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_52"},{"key":"e_1_3_2_1_41_1","first-page":"449","volume-title":"ICSE","author":"Weiser M.","unstructured":"M. Weiser . Program slicing . In ICSE , pages 439\u2013 449 . IEEE, 1981. M. Weiser. Program slicing. In ICSE, pages 439\u2013449. IEEE, 1981."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_26"},{"key":"e_1_3_2_1_43_1","first-page":"835","volume-title":"ASE","author":"Zheng M.","unstructured":"M. Zheng , M. S. Rogers , Z. Luo , M. B. Dwyer , and S. F. Siegel . CIVL: formal verification of parallel programs . In ASE , pages 830\u2013 835 . IEEE, 2015. M. Zheng, M. S. Rogers, Z. Luo, M. B. Dwyer, and S. F. Siegel. CIVL: formal verification of parallel programs. In ASE, pages 830\u2013835. IEEE, 2015."}],"event":{"name":"ASE'16: ACM\/IEEE International Conference on Automated Software Engineering","location":"Singapore Singapore","acronym":"ASE'16","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"]},"container-title":["Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2970276.2970309","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2970276.2970309","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:00Z","timestamp":1750218600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2970276.2970309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,25]]},"references-count":42,"alternative-id":["10.1145\/2970276.2970309","10.1145\/2970276"],"URL":"https:\/\/doi.org\/10.1145\/2970276.2970309","relation":{},"subject":[],"published":{"date-parts":[[2016,8,25]]},"assertion":[{"value":"2016-08-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}