{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T23:40:54Z","timestamp":1783554054494,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T00:00:00Z","timestamp":1740700800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Key Program of the National Natural Science Foundation of China","award":["62432010"],"award-info":[{"award-number":["62432010"]}]},{"name":"Beijing Institute of Control Engineering, Beijing Sunwise Information Technology Ltd, and by the Lab of High Confidence Embedded Software Engineering Technology","award":["No. YY-E-2022-KF"],"award-info":[{"award-number":["No. YY-E-2022-KF"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>Detecting atomicity violations effectively in interrupt-driven programs is difficult due to the asymmetric concurrency interleaving of interrupts. Current approaches face two main challenges: (1) A large number of false positives are generated by efficient static analysis techniques. (2) Loops with large or unknown bounds in these programs limit the scalability of the bounded verification techniques. To address these challenges, we present NIChecker, a new bounded verification tool designed to detect atomicity violations in interrupt-driven programs. The key ideas are: (1) Transforming an interrupt-driven program into a bounded sequential C program through lazy sequentialization technique. This sequential program accurately models interrupt masking and nested interrupt execution. (2) Combining a refined loop abstraction technique with our sequentialization to enhance the efficiency of detecting programs with intractable loops. (3) Integrating slicing and an interleaving path reduction technique known as preemption point reduction in NIChecker to shrink the explored state space. We prove the bounded correctness of our translation and discuss the impact of our optimizations. We evaluate NIChecker on 31 academic benchmark programs and 18 real-world interrupt-driven programs. Our results show that NIChecker achieves better precision, a lower false positive rate, and a significant verification speed-up than related state-of-the-art tools.<\/jats:p>","DOI":"10.1145\/3705311","type":"journal-article","created":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T16:08:21Z","timestamp":1732291701000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Bounded Verification of Atomicity Violations for Interrupt-Driven Programs via Lazy Sequentialization"],"prefix":"10.1145","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2386-4818","authenticated-orcid":false,"given":"Yuan","family":"Zhang","sequence":"first","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4920-0173","authenticated-orcid":false,"given":"Lei","family":"Qu","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8590-2434","authenticated-orcid":false,"given":"Yifei","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1913-4467","authenticated-orcid":false,"given":"Leihuan","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0874","authenticated-orcid":false,"given":"Tingting","family":"Yu","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5762-3749","authenticated-orcid":false,"given":"Rui","family":"Chen","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4338-5927","authenticated-orcid":false,"given":"Weiqiang","family":"Kong","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,2,28]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"e_1_3_2_5_2","first-page":"99","article-title":"Bounded model checking","volume":"185","author":"Biere Armin","year":"2009","unstructured":"Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. 2009. Bounded model checking. Handbook of Satisfiability 185, 99 (2009), 457\u2013481.","journal-title":"Handbook of Satisfiability"},{"issue":"10","key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"1693","DOI":"10.1016\/j.jss.2011.04.054","article-title":"On software verification for sensor nodes","volume":"84","author":"Bucur Doina","year":"2011","unstructured":"Doina Bucur and Marta Kwiatkowska. 2011. On software verification for sensor nodes. Journal of Systems and Software 84, 10 (2011), 1693\u20131707.","journal-title":"Journal of Systems and Software"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.13328\/j.cnki.jos.004980"},{"key":"e_1_3_2_8_2","first-page":"573","volume-title":"Proceedings of the International Symposium on Formal Methods","author":"Chimdyalwar Bharti","year":"2015","unstructured":"Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani, and Avriti Chauhan. 2015. Eliminating static analysis false positives using loop abstraction and bounded model checking. In Proceedings of the International Symposium on Formal Methods. Springer, 573\u2013576."},{"key":"e_1_3_2_9_2","first-page":"697","volume-title":"Proceedings of the European Symposium on Programming","author":"Chopra Nikita","year":"2019","unstructured":"Nikita Chopra, Rekha Pai, and Deepak D\u2019Souza. 2019. Data races and static analysis for interrupt-driven kernels. In Proceedings of the European Symposium on Programming, Vol. 11423, Springer, 697\u2013723."},{"key":"e_1_3_2_10_2","volume-title":"Program Slicing for Design Automation: An Automatic Technique for Speeding-up Hardware Design, Simulation, Testing, and Verification","author":"Clarke E. M.","year":"1998","unstructured":"E. M. Clarke, M. Fujita, S. P. Rajan, T. Reps, S. Shankar, and T. Teitelbaum. 1998. Program Slicing for Design Automation: An Automatic Technique for Speeding-up Hardware Design, Simulation, Testing, and Verification. Unpublished Report, Computer Sciences Department, University of Wisconsin-Madison."},{"key":"e_1_3_2_11_2","first-page":"168","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke Edmund","year":"2004","unstructured":"Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 168\u2013176."},{"key":"e_1_3_2_12_2","first-page":"1407","volume-title":"Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE)","author":"Darke Priyanka","year":"2015","unstructured":"Priyanka Darke, Bharti Chimdyalwar, R. Venkatesh, Ulka Shrotri, and Ravindra Metta. 2015. Over-approximating loops to prove properties using bounded model checking. In Proceedings of the Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1407\u20131412."},{"issue":"7","key":"e_1_3_2_13_2","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","article-title":"A survey of automated techniques for formal software verification","volume":"27","author":"D\u2019silva Vijay","year":"2008","unstructured":"Vijay D\u2019silva, Daniel Kroening, and Georg Weissenbacher. 2008. A survey of automated techniques for formal software verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27, 7 (2008), 1165\u20131178.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_2_14_2","first-page":"253","volume-title":"Proceedings of the 28th Asia-Pacific Software Engineering Conference.","author":"Du Xiang","year":"2021","unstructured":"Xiang Du, Liangze Yin, Haining Feng, and Wei Dong. 2021. Program verification enhanced precise analysis of interrupt-driven program vulnerabilities. In Proceedings of the 28th Asia-Pacific Software Engineering Conference. IEEE, 253\u2013263. DOI: 10.1109\/APSEC53868.2021.00033"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"1361","DOI":"10.1145\/3324884.3418925","volume-title":"Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering.","author":"Feng Haining","year":"2020","unstructured":"Haining Feng. 2020. A program verification based approach to find data race vulnerabilities in interrupt-driven program. In Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering. IEEE, 1361\u20131363. DOI: 10.1145\/3324884.3418925"},{"key":"e_1_3_2_16_2","first-page":"465","volume-title":"Proceedings of the 20th IEEE International Conference on Software Quality, Reliability and Security Companion (QRS).","author":"Feng Haining","year":"2020","unstructured":"Haining Feng, Liangze Yin, Wenfeng Lin, Xudong Zhao, and Wei Dong. 2020. Rchecker: A CBMC-based data race detector for interrupt-driven programs. In Proceedings of the 20th IEEE International Conference on Software Quality, Reliability and Security Companion (QRS). IEEE, 465\u2013471. DOI: 10.1109\/QRS-C51114.2020.00084"},{"issue":"3","key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/24039.24041","article-title":"The program dependence graph and its use in optimization","volume":"9","author":"Ferrante Jeanne","year":"1987","unstructured":"Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems 9, 3 (1987), 319\u2013349.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_18_2","first-page":"710","volume-title":"Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Fischer Bernd","year":"2013","unstructured":"Bernd Fischer, Omar Inverso, and Gennaro Parlato. 2013. CSeq: A concurrency pre-processor for sequential C verification tools. In Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 710\u2013713."},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1145\/1808266.1808278","volume-title":"Proceedings of the 5th Workshop on Automation of Software Test","author":"Higashi Makoto","year":"2010","unstructured":"Makoto Higashi, Tetsuo Yamamoto, Yasuhiro Hayase, Takashi Ishio, and Katsuro Inoue. 2010. An effective method to control interrupt handler for data race detection. In Proceedings of the 5th Workshop on Automation of Software Test, 79\u201386."},{"key":"e_1_3_2_20_2","first-page":"807","volume-title":"Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Inverso Omar","year":"2015","unstructured":"Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2015. Lazy-cseq: A context-bounded model checking tool for multi-threaded c-programs. In Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 807\u2013812."},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-319-08867-9_39","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Inverso Omar","year":"2014","unstructured":"Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded model checking of multi-threaded C programs via lazy sequentialization. In Proceedings of the International Conference on Computer Aided Verification. Springer, 585\u2013602."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3478536"},{"key":"e_1_3_2_23_2","first-page":"229","volume-title":"Proceedings of the Design, Automation & Test in Europe Conference","author":"Kroening Daniel","year":"2015","unstructured":"Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. 2015. Effective verification of low-level software with nested interrupts. In Proceedings of the Design, Automation & Test in Europe Conference. ACM, New York, NY, 229\u2013234. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=2755803"},{"key":"e_1_3_2_24_2","first-page":"94","volume-title":"Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering","author":"Lai Zhifeng","year":"2008","unstructured":"Zhifeng Lai, Shing-Chi Cheung, and Wing Kwong Chan. 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. ACM, New York, NY, 94\u2013104."},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","article-title":"Reducing concurrent analysis under a context bound to sequential analysis","volume":"35","author":"Lal Akash","year":"2009","unstructured":"Akash Lal and Thomas Reps. 2009. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35 (2009), 73\u201397.","journal-title":"Formal Methods in System Design"},{"key":"e_1_3_2_26_2","first-page":"506","volume-title":"Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"Li Chao","year":"2022","unstructured":"Chao Li, Rui Chen, Boxiang Wang, Tingting Yu, Dongdong Gao, and Mengfei Yang. 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, 506\u2013518. DOI: 10.1145\/3533767.3534412"},{"issue":"2","key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3147432","article-title":"Effective verification for low-level software with competing interrupts","volume":"17","author":"Liang Lihao","year":"2017","unstructured":"Lihao Liang, Tom Melham, Daniel Kroening, Peter Schrammel, and Michael Tautschnig. 2017. Effective verification for low-level software with competing interrupts. ACM Transactions on Embedded Computing Systems 17, 2 (2017), 1\u201326.","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"e_1_3_2_28_2","first-page":"193","volume-title":"Proceedings of the Theoretical Aspects of Software Engineering Conference","author":"Liu Han","year":"2014","unstructured":"Han Liu, Hehua Zhang, Yu Jiang, Xiaoyu Song, Ming Gu, and Jiaguang Sun. 2014. iDola: Bridge modeling to verification and implementation of interrupt-driven systems. In Proceedings of the Theoretical Aspects of Software Engineering Conference. IEEE, 193\u2013200."},{"key":"e_1_3_2_29_2","first-page":"37","volume-title":"Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS \u201906)","author":"Lu Shan","year":"2006","unstructured":"Shan Lu, Joseph A. Tucek, Feng Qin, and Yuanyuan Zhou. 2006. AVIO: detecting atomicity violations via access interleaving invariants. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS \u201906). John Paul Shen and Margaret Martonosi (Eds.), ACM, New York, NY, 37\u201348."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/11871743"},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-319-46520-3_12","volume-title":"Proceedings of International Symposium on Automated Technology for Verification and Analysis","author":"Nguyen Truc L.","year":"2016","unstructured":"Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2016. Lazy sequentialization for the safety verification of unbounded concurrent programs. In Proceedings of International Symposium on Automated Technology for Verification and Analysis, Springer, 174\u2013191."},{"key":"e_1_3_2_32_2","first-page":"255","volume-title":"Proceedings of 5th International Conference on Networked Systems (NETYS \u201917)","author":"Nguyen Truc L.","year":"2017","unstructured":"Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2017. Concurrent program verification with lazy sequentialization and interval analysis. In Proceedings of 5th International Conference on Networked Systems (NETYS \u201917). Springer, 255\u2013271."},{"key":"e_1_3_2_33_2","first-page":"212","volume-title":"Proceedings of the 41st International Conference on Software Engineering","author":"Pan Minxue","year":"2019","unstructured":"Minxue Pan, Shouyu Chen, Yu Pei, Tian Zhang, and Xuandong Li. 2019. Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In Proceedings of the 41st International Conference on Software Engineering. IEEE\/ACM, New York, NY, 212\u2013222. DOI: 10.1109\/ICSE.2019.00037"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1145\/1086228.1086282","volume-title":"Proceedings of the 5th ACM International Conference On Embedded Software","author":"Regehr John","year":"2005","unstructured":"John Regehr. 2005. Random testing of interrupt-driven software. In Proceedings of the 5th ACM International Conference On Embedded Software. ACM, New York, NY, 290\u2013298. DOI: 10.1145\/1086228.1086282"},{"issue":"9","key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/j.entcs.2007.04.002","article-title":"Interrupt verification via thread verification","volume":"174","author":"Regehr John","year":"2007","unstructured":"John Regehr and Nathan Cooprider. 2007. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science 174, 9 (2007), 139\u2013150.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-642-19237-1_5","volume-title":"Proceedings of the 5th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC)","author":"Schlich Bastian","year":"2011","unstructured":"Bastian Schlich, Thomas Noll, J\u00f6rg Brauer, and Lucas Brutschy. 2011. Reduction of interrupt handler executions for model checking embedded software. In Proceedings of the 5th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC). Springer, 5\u201320."},{"key":"e_1_3_2_37_2","first-page":"206","volume-title":"Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering","author":"Sung Chungha","year":"2017","unstructured":"Chungha Sung, Markus Kusano, and Chao Wang. 2017. Modular verification of interrupt-driven software. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering. IEEE Computer Society, 206\u2013216. DOI: 10.1109\/ASE.2017.8115634"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-642-35585-1_20","volume-title":"Proceedings of the 4th International Conference on Future Generation Information Technology (FGIT \u201912)","author":"Tchamgoue Guy Martin","year":"2012","unstructured":"Guy Martin Tchamgoue, Kyong Hoon Kim, and Yong-Kee Jun. 2012. Dynamic race detection techniques for interrupt-driven programs. In Proceedings of the 4th International Conference on Future Generation Information Technology (FGIT \u201912). Springer, 148\u2013153."},{"key":"e_1_3_2_39_2","first-page":"11","article-title":"Verification of data races in concurrent interrupt handlers","volume":"9","author":"Tchamgoue Guy Martin","year":"2013","unstructured":"Guy Martin Tchamgoue, Kyong Hoon Kim, and Yong-Kee Jun. 2013. Verification of data races in concurrent interrupt handlers. International Journal of Distributed Sensor Networks 9, 11 (2013), 953593.","journal-title":"International Journal of Distributed Sensor Networks"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1109\/CSMR.1997.583007","volume-title":"Proceedings of the 1st Euromicro Working Conference on Software Maintenance and Reengineering (CSMR \u201997)","author":"Tonella Paolo","year":"1997","unstructured":"Paolo Tonella, Giuliano Antoniol, Roberto Fiutem, and Ettore Merlo. 1997. Variable precision reaching definitions analysis for software maintenance. In Proceedings of the 1st Euromicro Working Conference on Software Maintenance and Reengineering (CSMR \u201997). IEEE Computer Society, 60\u201367."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2989171"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1145\/2875913.2875943","volume-title":"Proceedings of the 7th Asia-Pacific Symposium on Internetware","author":"Wang Yu","year":"2015","unstructured":"Yu Wang, Junjing Shi, Linzhang Wang, Jianhua Zhao, and Xuandong Li. 2015. Detecting data races in interrupt-driven programs based on static analysis and dynamic simulation. In Proceedings of the 7th Asia-Pacific Symposium on Internetware, 199\u2013202."},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/3092703.3092724","volume-title":"Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"Wang Yu","year":"2017","unstructured":"Yu Wang, Linzhang Wang, Tingting Yu, Jianhua Zhao, and Xuandong Li. 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, 113\u2013124."},{"key":"e_1_3_2_44_2","first-page":"55","volume-title":"Proceedings of the International Conference on Embedded Software (EMSOFT)","author":"Wu Xueguang","year":"2015","unstructured":"Xueguang Wu, Liqian Chen, Antoine Min\u00e9, Wei Dong, and Ji Wang. 2015. Numerical static analysis of interrupt-driven programs via sequentialization. In Proceedings of the International Conference on Embedded Software (EMSOFT). IEEE, 55\u201364."},{"key":"e_1_3_2_45_2","first-page":"204","volume-title":"Proceedings of the IEEE 7th International Conference on Software Security and Reliability Companion","author":"Wu Xueguang","year":"2013","unstructured":"Xueguang Wu, Yanjun Wen, Liqian Chen, Wei Dong, and Ji Wang. 2013. Data race detection for interrupt-driven programs via bounded model checking. In Proceedings of the IEEE 7th International Conference on Software Security and Reliability Companion. IEEE, 204\u2013210."},{"key":"e_1_3_2_46_2","first-page":"1153","volume-title":"Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","author":"Yu Bin","year":"2023","unstructured":"Bin Yu, Cong Tian, Hengrui Xing, Zuchao Yang, Jie Su, Xu Lu, Jiyu Yang, Liang Zhao, Xiaofeng Li, and Zhenhua Duan. 2023. Detecting atomicity violations in interrupt-driven programs via interruption points selecting and delayed ISR-triggering. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM, New York, NY, 1153\u20131164."},{"key":"e_1_3_2_47_2","first-page":"69","article-title":"Precise dynamic data race prediction for interrupt-driven embedded software","author":"Yu Tingting","year":"2023","unstructured":"Tingting Yu, Chunpeng Jia, Rui Chen, Chao Li, Boxiang Wang, and Yunsong Jiang. 2023. Precise dynamic data race prediction for interrupt-driven embedded software. In Proceedings of the IEEE 34th International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE, 69\u201374.","journal-title":"Proceedings of the IEEE 34th International Symposium on Software Reliability Engineering Workshops (ISSREW)"},{"key":"e_1_3_2_48_2","first-page":"51","volume-title":"Proceedings of the 8th International Conference on Virtual Execution Environments, VEE","author":"Yu Tingting","year":"2012","unstructured":"Tingting Yu, Witawas Srisa-an, and Gregg Rothermel. 2012. SimTester: A controllable and observable testing framework for embedded systems. In Proceedings of the 8th International Conference on Virtual Execution Environments, VEE. ACM, New York, NY, 51\u201362."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3705311","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3705311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:02Z","timestamp":1750295882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3705311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,28]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3705311"],"URL":"https:\/\/doi.org\/10.1145\/3705311","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,28]]},"assertion":[{"value":"2024-07-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-05","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}