{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:09:00Z","timestamp":1750306140186,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":69,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T00:00:00Z","timestamp":1499644800000},"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":[[2017,7,10]]},"DOI":"10.1145\/3092703.3092724","type":"proceedings-article","created":{"date-parts":[[2017,7,11]],"date-time":"2017-07-11T20:17:18Z","timestamp":1499804238000},"page":"113-124","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Automatic detection and validation of race conditions in interrupt-driven embedded software"],"prefix":"10.1145","author":[{"given":"Yu","family":"Wang","sequence":"first","affiliation":[{"name":"Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linzhang","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tingting","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Kentucky, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/clanganalyzer .llvm.org","author":"Analyzer Clang Static","year":"2016","unstructured":"Clang Static Analyzer . https:\/\/clanganalyzer .llvm.org , 2016 . Clang Static Analyzer. https:\/\/clanganalyzer .llvm.org, 2016."},{"key":"e_1_3_2_1_2_1","volume-title":"https:\/\/klee .github.io\/","author":"Execution Engine KLEE LLVM","year":"2016","unstructured":"KLEE LLVM Execution Engine . https:\/\/klee .github.io\/ , 2016 . KLEE LLVM Execution Engine. https:\/\/klee .github.io\/, 2016."},{"volume-title":"https:\/\/github .com\/klee\/klee-uclibc","year":"2016","unstructured":"KLEE-uClibc. https:\/\/github .com\/klee\/klee-uclibc , 2016 . KLEE-uClibc. https:\/\/github .com\/klee\/klee-uclibc, 2016.","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","volume-title":"http:\/\/stp .github.io\/","author":"STP","year":"2016","unstructured":"STP constraint solver. http:\/\/stp .github.io\/ , 2016 . STP constraint solver. http:\/\/stp .github.io\/, 2016."},{"unstructured":"Thread safety analysis 2016. http:\/\/clang.llvm.org\/docs\/ThreadSafetyAnalysis.html.  Thread safety analysis 2016. http:\/\/clang.llvm.org\/docs\/ThreadSafetyAnalysis.html.","key":"e_1_3_2_1_5_1"},{"key":"e_1_3_2_1_6_1","volume-title":"http:\/\/clang .llvm.org\/docs\/ClangTools.html","author":"Using Clang","year":"2016","unstructured":"Using Clang Tools - LLVM. http:\/\/clang .llvm.org\/docs\/ClangTools.html , 2016 . Using Clang Tools - LLVM. http:\/\/clang .llvm.org\/docs\/ClangTools.html, 2016."},{"key":"e_1_3_2_1_7_1","first-page":"37","volume-title":"Theorem Proving in Higher Order Logics","author":"Aspinall D.","unstructured":"D. Aspinall and J. \u0160ev\u010d\u00edk . Formalising java\u00e2\u0102\u0179s data race free guarantee . In Theorem Proving in Higher Order Logics , pages 22\u2013 37 . Springer, 2007. D. Aspinall and J. \u0160ev\u010d\u00edk. Formalising java\u00e2\u0102\u0179s data race free guarantee. In Theorem Proving in Higher Order Logics, pages 22\u201337. Springer, 2007."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/2814270.2814303"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1145\/1806596.1806626"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_3_2_1_11_1","first-page":"224","volume-title":"KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In USENIX Symposium on Operating Systems Design and Implementations (OSDI)","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In USENIX Symposium on Operating Systems Design and Implementations (OSDI) , pages 209\u2013 224 , 2008 . C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In USENIX Symposium on Operating Systems Design and Implementations (OSDI), pages 209\u2013224, 2008."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1145\/99164.99167"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1109\/SSIRI-C.2011.18"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1145\/1693453.1693458"},{"key":"e_1_3_2_1_15_1","volume-title":"Linux device drivers. \" O\u2019Reilly Media","author":"Corbet J.","year":"2005","unstructured":"J. Corbet , A. Rubini , and G. Kroah-Hartman . Linux device drivers. \" O\u2019Reilly Media , Inc .\", 2005 . J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux device drivers. \" O\u2019Reilly Media, Inc.\", 2005."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/120807.120811"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1145\/2384616.2384650"},{"unstructured":"J. Engblom. Systematically exposing os kernel races - an interview with ben blum 2012. http:\/\/blogs.windriver.com\/tools\/2012\/09\/systematically-exposingos-kernel-races-an-interview-with-ben-blum.html.  J. Engblom. Systematically exposing os kernel races - an interview with ben blum 2012. http:\/\/blogs.windriver.com\/tools\/2012\/09\/systematically-exposingos-kernel-races-an-interview-with-ben-blum.html.","key":"e_1_3_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1145\/2491411.2491453"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1145\/781131.781169"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/2786805.2786841"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1145\/1808266.1808278"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/1808266.1808278"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1109\/ICST.2014.17"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1002\/stvr.1539"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1145\/2594291.2594330"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1145\/2931037.2931069"},{"key":"e_1_3_2_1_28_1","first-page":"016","article-title":"Static race detection of interrupt-driven programs","volume":"12","author":"Huo W.","year":"2011","unstructured":"W. Huo , H. Yu , X. Feng , and Z. Zhang . Static race detection of interrupt-driven programs . Journal of Computer Research and Development , 12 : 016 , 2011 . W. Huo, H. Yu, X. Feng, and Z. Zhang. Static race detection of interrupt-driven programs. Journal of Computer Research and Development, 12:016, 2011.","journal-title":"Journal of Computer Research and Development"},{"unstructured":"I. Jackson. IRQ handling race and spurious IIR read in 8250.c. Web page. https:\/\/lkml.org\/lkml\/2009\/3\/12\/379.  I. Jackson. IRQ handling race and spurious IIR read in 8250.c. Web page. https:\/\/lkml.org\/lkml\/2009\/3\/12\/379.","key":"e_1_3_2_1_29_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1145\/2103656.2103662"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_31_1","DOI":"10.1145\/1595696.1595701"},{"key":"e_1_3_2_1_32_1","first-page":"90","volume-title":"Formal Method in Computer-Aided Design (FMCAD)","author":"Kotker J.","year":"2011","unstructured":"J. Kotker , D. Sadigh , and S. A. Seshia . Timing analysis of interrupt-driven programs under context bounds . In Formal Method in Computer-Aided Design (FMCAD) , pages 81\u2013 90 , 2011 . J. Kotker, D. Sadigh, and S. A. Seshia. Timing analysis of interrupt-driven programs under context bounds. In Formal Method in Computer-Aided Design (FMCAD), pages 81\u201390, 2011."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1145\/2254064.2254088"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1145\/1453101.1453115"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1145\/2594291.2594311"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1145\/1047659.1040336"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.5555\/2337223.2337308"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1145\/1542476.1542491"},{"key":"e_1_3_2_1_39_1","first-page":"280","volume-title":"USENIX Symposium on Operating Systems Design and Implementations (OSDI)","author":"Musuvathi M.","year":"2008","unstructured":"M. Musuvathi , S. Qadeer , T. Ball , G. Basler , P. A. Nainar , and I. Neamtiu . Finding and reproducing Heisenbugs in concurrent programs . In USENIX Symposium on Operating Systems Design and Implementations (OSDI) , pages 267\u2013 280 , 2008 . M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In USENIX Symposium on Operating Systems Design and Implementations (OSDI), pages 267\u2013280, 2008."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.1109\/ICSE.2009.5070538"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_41_1","DOI":"10.5555\/2337223.2337309"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.1145\/966049.781528"},{"unstructured":"L. Osterman. Larry Gets Taken to Task on Concurrency 2005.  L. Osterman. Larry Gets Taken to Task on Concurrency 2005.","key":"e_1_3_2_1_43_1"},{"unstructured":"https:\/\/blogs.msdn.microsoft.com\/larryosterman\/2005\/02\/11\/larry-gets-takento-task-on-concurrency\/.  https:\/\/blogs.msdn.microsoft.com\/larryosterman\/2005\/02\/11\/larry-gets-takento-task-on-concurrency\/.","key":"e_1_3_2_1_44_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","DOI":"10.1145\/966049.781529"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_46_1","DOI":"10.1145\/2254064.2254126"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_47_1","DOI":"10.1145\/2254064.2254127"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_48_1","DOI":"10.1145\/2544173.2509538"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_49_1","DOI":"10.1145\/1086228.1086282"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_50_1","DOI":"10.1016\/j.entcs.2007.04.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_51_1","DOI":"10.1145\/2813885.2737998"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_52_1","DOI":"10.1145\/2983990.2984040"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_53_1","DOI":"10.1145\/265924.265927"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_54_1","DOI":"10.1145\/1321631.1321679"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_55_1","DOI":"10.1145\/1375581.1375584"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_56_1","DOI":"10.1007\/11817963_38"},{"key":"e_1_3_2_1_57_1","volume-title":"Which CP Us Can Do Atomic 16B Memory Operations?","author":"Instructions SSE","year":"2014","unstructured":"SSE Instructions : Which CP Us Can Do Atomic 16B Memory Operations? , 2014 . http:\/\/stackoverflow.com\/questions\/7646018\/sse-instructions-which-cpus-cando-atomic-16b-memory-operations. SSE Instructions: Which CP Us Can Do Atomic 16B Memory Operations?, 2014. http:\/\/stackoverflow.com\/questions\/7646018\/sse-instructions-which-cpus-cando-atomic-16b-memory-operations."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_58_1","DOI":"10.1145\/237721.237727"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_59_1","DOI":"10.1023\/A:1022920129859"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_60_1","DOI":"10.1145\/2970276.2970337"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_61_1","DOI":"10.1145\/781131.781145"},{"unstructured":"ISSTA\u201917 July 10-14 2017 Santa Barbara CA USA Yu Wang Linzhang Wang Tingting Yu Jianhua Zhao and Xuandong LI  ISSTA\u201917 July 10-14 2017 Santa Barbara CA USA Yu Wang Linzhang Wang Tingting Yu Jianhua Zhao and Xuandong LI","key":"e_1_3_2_1_62_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_63_1","DOI":"10.1145\/2875913.2875943"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_64_1","DOI":"10.1145\/996841.996859"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_65_1","DOI":"10.1007\/11531142_26"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_66_1","DOI":"10.1145\/2384616.2384651"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_67_1","DOI":"10.1145\/2884781.2884866"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_68_1","DOI":"10.1145\/2365864.2151034"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_69_1","DOI":"10.1145\/1095809.1095832"}],"event":{"sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"acronym":"ISSTA '17","name":"ISSTA '17: International Symposium on Software Testing and Analysis","location":"Santa Barbara CA USA"},"container-title":["Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092703.3092724","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092703.3092724","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:26Z","timestamp":1750217846000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092703.3092724"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,10]]},"references-count":69,"alternative-id":["10.1145\/3092703.3092724","10.1145\/3092703"],"URL":"https:\/\/doi.org\/10.1145\/3092703.3092724","relation":{},"subject":[],"published":{"date-parts":[[2017,7,10]]},"assertion":[{"value":"2017-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}