{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T15:28:44Z","timestamp":1773156524671,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"15","license":[{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100005046","name":"Natural Science Foundation of Heilongjiang Province","doi-asserted-by":"publisher","award":["JJ2019LH2160"],"award-info":[{"award-number":["JJ2019LH2160"]}],"id":[{"id":"10.13039\/501100005046","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2024,10]]},"DOI":"10.1007\/s11227-024-06189-4","type":"journal-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T16:02:13Z","timestamp":1718380933000},"page":"21699-21725","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Efficient data race detection for interrupt-driven programs via path feasibility analysis"],"prefix":"10.1007","volume":"80","author":[{"given":"Jingwen","family":"Zhao","sequence":"first","affiliation":[]},{"given":"Yanxia","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Jibin","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"key":"6189_CR1","unstructured":"Kotker J, Sadigh D, Seshia SA (2011) Timing analysis of interrupt-driven programs under context bounds. In: 2011 Formal methods in computer-aided design (FMCAD), pp 81\u201390. IEEE"},{"key":"6189_CR2","doi-asserted-by":"crossref","unstructured":"Mukherjee S, Kumar A, D\u2019Souza D (2017) Detecting all high-level dataraces in an rtos kernel. In: Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15\u201317, 2017, Proceedings 18, pp 405\u2013423. Springer","DOI":"10.1007\/978-3-319-52234-0_22"},{"key":"6189_CR3","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/s11219-017-9385-3","volume":"26","author":"H Fu","year":"2018","unstructured":"Fu H, Wang Z, Chen X, Fan X (2018) A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniques. Softw Qual J 26:855\u2013889","journal-title":"Softw Qual J"},{"key":"6189_CR4","doi-asserted-by":"crossref","unstructured":"Yu T, Cohen M (2015) Guided test generation for finding worst-case stack usage in embedded systems. In: 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST), pp 1\u201310. IEEE","DOI":"10.1109\/ICST.2015.7102592"},{"key":"6189_CR5","unstructured":"Poulsen K (2004) Software bug contributed to blackout. Security Focus"},{"key":"6189_CR6","doi-asserted-by":"crossref","unstructured":"Regehr J (2005) Random testing of interrupt-driven software. In: Proceedings of the 5th ACM International Conference on Embedded Software, pp 290\u2013298","DOI":"10.1145\/1086228.1086282"},{"key":"6189_CR7","doi-asserted-by":"crossref","unstructured":"Lai Z, Cheung S-C, Chan WK (2008) Inter-context control-flow and data-flow test adequacy criteria for nesc applications. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp 94\u2013104","DOI":"10.1145\/1453101.1453115"},{"issue":"9","key":"6189_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2007.04.002","volume":"174","author":"J Regehr","year":"2007","unstructured":"Regehr J, Cooprider N (2007) Interrupt verification via thread verification. Electron Notes Theor Comput Sci 174(9):139\u2013150","journal-title":"Electron Notes Theor Comput Sci"},{"key":"6189_CR9","doi-asserted-by":"crossref","unstructured":"Wu X, Wen Y, Chen L, Dong W, Wang J (2013) Data race detection for interrupt-driven programs via bounded model checking. In: 2013 IEEE Seventh International Conference on Software Security and Reliability Companion, pp 204\u2013210. IEEE","DOI":"10.1109\/SERE-C.2013.33"},{"issue":"1","key":"6189_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/1925844.1926398","volume":"46","author":"MD Schwarz","year":"2011","unstructured":"Schwarz MD, Seidl H, Vojdani V, Lammich P, M\u00fcller-Olm M (2011) Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. ACM SIGPLAN Not 46(1):93\u2013104","journal-title":"ACM SIGPLAN Not"},{"issue":"4","key":"6189_CR11","first-page":"1","volume":"15","author":"X Wu","year":"2016","unstructured":"Wu X, Chen L, Min\u00e9 A, Dong W, Wang J (2016) Static analysis of runtime errors in interrupt-driven programs via sequentialization. ACM Trans Embed Comput Syst (TECS) 15(4):1\u201326","journal-title":"ACM Trans Embed Comput Syst (TECS)"},{"key":"6189_CR12","doi-asserted-by":"crossref","unstructured":"Yu T, Srisa-an W, Rothermel G (2012) Simtester: a controllable and observable testing framework for embedded systems. In: Proceedings of the 8th ACM SIGPLAN\/SIGOPS Conference on Virtual Execution Environments, pp 51\u201362","DOI":"10.1145\/2151024.2151034"},{"issue":"5","key":"6189_CR13","doi-asserted-by":"publisher","first-page":"8945","DOI":"10.1109\/JIOT.2019.2925291","volume":"6","author":"Y Sun","year":"2019","unstructured":"Sun Y, Cheung S-C, Guo S, Cheng M (2019) Disclosing and locating concurrency bugs of interrupt-driven IoT programs. IEEE Internet Things J 6(5):8945\u20138957","journal-title":"IEEE Internet Things J"},{"issue":"1","key":"6189_CR14","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1109\/TSE.2020.2989171","volume":"48","author":"Y Wang","year":"2020","unstructured":"Wang Y, Gao F, Wang L, Yu T, Zhao J, Li X (2020) Automatic detection, validation, and repair of race conditions in interrupt-driven embedded software. IEEE Trans Softw Eng 48(1):346\u2013363","journal-title":"IEEE Trans Softw Eng"},{"key":"6189_CR15","doi-asserted-by":"crossref","unstructured":"Sung C, Kusano M, Wang C (2017) Modular verification of interrupt-driven software. In: 2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp 206\u2013216. IEEE","DOI":"10.1109\/ASE.2017.8115634"},{"key":"6189_CR16","doi-asserted-by":"crossref","unstructured":"Wang Y, Wang L, Yu T, Zhao J, Li X (2017) Automatic detection and validation of race conditions in interrupt-driven embedded software. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp 113\u2013124","DOI":"10.1145\/3092703.3092724"},{"key":"6189_CR17","doi-asserted-by":"crossref","unstructured":"Feng H, Yin L, Lin W, Zhao X, Dong W (2020) Rchecker: A cbmc-based data race detector for interrupt-driven programs. In: 2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C), pp 465\u2013471. IEEE","DOI":"10.1109\/QRS-C51114.2020.00084"},{"key":"6189_CR18","doi-asserted-by":"crossref","unstructured":"Chen R, Guo X, Duan Y, Gu B, Yang M (2011) Static data race detection for interrupt-driven embedded software. In: 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement-Companion, pp 47\u201352. IEEE","DOI":"10.1109\/SSIRI-C.2011.18"},{"key":"6189_CR19","doi-asserted-by":"crossref","unstructured":"Chopra N, Pai R, D\u2019Souza D (2019) Data races and static analysis for interrupt-driven kernels. In: Programming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings 28, pp 697\u2013723. Springer","DOI":"10.1007\/978-3-030-17184-1_25"},{"key":"6189_CR20","doi-asserted-by":"crossref","unstructured":"Li C, Chen R, Wang B, Yu T, Gao D, Yang M (2022) Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruning. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pp 506\u2013518","DOI":"10.1145\/3533767.3534412"},{"issue":"5","key":"6189_CR21","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/1165389.945468","volume":"37","author":"D Engler","year":"2003","unstructured":"Engler D, Ashcraft K (2003) Racerx: effective, static detection of race conditions and deadlocks. ACM SIGOPS Oper Syst Rev 37(5):237\u2013252","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"6189_CR22","unstructured":"Chen R (2019) Racebench website. https:\/\/github.com\/chenruibuaa\/racebench"},{"key":"6189_CR23","unstructured":"Praun C (2011) Race detection techniques"},{"key":"6189_CR24","doi-asserted-by":"crossref","unstructured":"Huang Y, Zhao Y, Shi J, Zhu H, Qin S (2012) Investigating time properties of interrupt-driven programs. In: Formal Methods: Foundations and Applications: 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings 15, pp 131\u2013146. Springer","DOI":"10.1007\/978-3-642-33296-8_11"},{"issue":"6","key":"6189_CR25","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/1133255.1134019","volume":"41","author":"P Pratikakis","year":"2006","unstructured":"Pratikakis P, Foster JS, Hicks M (2006) Locksmith: context-sensitive correlation analysis for race detection. Acm Sigplan Not 41(6):320\u2013331","journal-title":"Acm Sigplan Not"},{"key":"6189_CR26","unstructured":"Marek C (2021) DG website. https:\/\/github.com\/mchalupa\/dg"},{"key":"6189_CR27","doi-asserted-by":"crossref","unstructured":"Shi Q, Xiao X, Wu R, Zhou J, Fan G, Zhang C (2018) Pinpoint: Fast and precise sparse value flow analysis for million lines of code. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 693\u2013706","DOI":"10.1145\/3192366.3192418"},{"key":"6189_CR28","unstructured":"Lattner C (2008) Llvm and clang: next generation compiler technology. In: The BSD Conference, vol 5, pp 1\u201320"},{"key":"6189_CR29","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14, pp 337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6189_CR30","volume-title":"Linux device drivers","author":"J Corbet","year":"2005","unstructured":"Corbet J, Rubini A, Kroah-Hartman G (2005) Linux device drivers. O\u2019Reilly Media, Inc."},{"issue":"12","key":"6189_CR31","first-page":"5120","volume":"48","author":"J-J Bai","year":"2021","unstructured":"Bai J-J, Chen Q-L, Jiang Z-M, Lawall J, Hu S-M (2021) Hybrid static-dynamic analysis of data races caused by inconsistent locking discipline in device drivers. IEEE Trans Softw Eng 48(12):5120\u20135135","journal-title":"IEEE Trans Softw Eng"},{"key":"6189_CR32","doi-asserted-by":"crossref","unstructured":"Wu X, Chen L, Min\u00e9 A, Dong W, Wang J (2015) Numerical static analysis of interrupt-driven programs via sequentialization. In: 2015 International Conference on Embedded Software (EMSOFT), pp 55\u201364. IEEE","DOI":"10.1109\/EMSOFT.2015.7318260"},{"key":"6189_CR33","doi-asserted-by":"crossref","unstructured":"Du X, Yin L, Feng H, Dong W (2021) Program verification enhanced precise analysis of interrupt-driven program vulnerabilities. In: 2021 28th Asia-Pacific Software Engineering Conference (APSEC), pp 253\u2013263. IEEE","DOI":"10.1109\/APSEC53868.2021.00033"},{"issue":"6","key":"6189_CR34","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1145\/2666356.2594330","volume":"49","author":"C-H Hsiao","year":"2014","unstructured":"Hsiao C-H, Yu J, Narayanasamy S, Kong Z, Pereira CL, Pokam GA, Chen PM, Flinn J (2014) Race detection for event-driven mobile applications. ACM SIGPLAN Not. 49(6):326\u2013336","journal-title":"ACM SIGPLAN Not."},{"key":"6189_CR35","doi-asserted-by":"crossref","unstructured":"Pan M, Chen S, Pei Y, Zhang T, Li X (2019) Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE), pp 212\u2013222. IEEE","DOI":"10.1109\/ICSE.2019.00037"},{"key":"6189_CR36","doi-asserted-by":"crossref","unstructured":"Schwarz MD, Seidl H, Vojdani V, Apinis K (2014) Precise analysis of value-dependent synchronization in priority scheduled programs. In: Verification, Model Checking, and Abstract Interpretation: 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings 15, pp 21\u201338. Springer","DOI":"10.1007\/978-3-642-54013-4_2"},{"key":"6189_CR37","doi-asserted-by":"crossref","unstructured":"Pai R, Singh A, D\u2019Souza D, D\u2019Souza M, Prakash P (2021) Static analysis for detecting high-level races in rtos kernels. Formal Methods Syst Des, 1\u201328","DOI":"10.1007\/s10703-020-00354-0"},{"key":"6189_CR38","doi-asserted-by":"crossref","unstructured":"Park S (2013) Fault comprehension for concurrent programs. In: 2013 35th International Conference on Software Engineering (ICSE), pp 1444\u20131446. IEEE","DOI":"10.1109\/ICSE.2013.6606739"},{"key":"6189_CR39","doi-asserted-by":"crossref","unstructured":"Higashi M, Yamamoto T, Hayase Y, Ishio T, Inoue K (2010) An effective method to control interrupt handler for data race detection. In: Proceedings of the 5th Workshop on Automation of Software Test, pp 79\u201386","DOI":"10.1145\/1808266.1808278"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-024-06189-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11227-024-06189-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-024-06189-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,12]],"date-time":"2024-08-12T09:14:06Z","timestamp":1723454046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11227-024-06189-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,14]]},"references-count":39,"journal-issue":{"issue":"15","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["6189"],"URL":"https:\/\/doi.org\/10.1007\/s11227-024-06189-4","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,14]]},"assertion":[{"value":"3 May 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interest"}}]}}