{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:01:26Z","timestamp":1754161286196,"version":"3.41.2"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,23]]},"DOI":"10.1145\/3696630.3728592","type":"proceedings-article","created":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:09:27Z","timestamp":1753729767000},"page":"1114-1118","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["SpecChecker-Int: An Extensible Concurrency Bugs Detection Tool for Interrupt-driven Embedded Software"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6960-0421","authenticated-orcid":false,"given":"Boxiang","family":"Wang","sequence":"first","affiliation":[{"name":"Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1170-587X","authenticated-orcid":false,"given":"Chao","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering and Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-9645-4659","authenticated-orcid":false,"given":"Sheng","family":"Wang","sequence":"additional","affiliation":[{"name":"Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1127-3534","authenticated-orcid":false,"given":"Chunpeng","family":"Jia","sequence":"additional","affiliation":[{"name":"Beijing Sunwise Information Technology Ltd, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6844-1246","authenticated-orcid":false,"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[{"name":"China Academy of Space Technology, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,7,28]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2015. China Academy of Space Technology Software Product Assurance Center. Analysis Report on Software Quality Problems of China Academy of Space Technology."},{"key":"e_1_3_2_1_2_1","unstructured":"2025. polyspace-bug-finder. https:\/\/www.mathworks.com\/products\/polyspace-bug-finder.html."},{"key":"e_1_3_2_1_3_1","unstructured":"2025. SpecChecker-Int. https:\/\/github.com\/wangilson\/SpecChecker-Int."},{"key":"e_1_3_2_1_4_1","volume-title":"2011 Fifth International Conference on Secure Software Integration and Reliability Improvement-Companion. IEEE, 47\u201352","author":"Chen Rui","year":"2011","unstructured":"Rui Chen, Xiangying Guo, Yonghao Duan, Bin Gu, and Mengfei Yang. 2011. Static data race detection for interrupt-driven embedded software. In 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement-Companion. IEEE, 47\u201352. 10.1109\/ssiri-c.2011.18"},{"key":"e_1_3_2_1_5_1","first-page":"547","article-title":"Interrupt data race detection based on shared variable access order pattern","volume":"3","author":"Chen Rui","year":"2016","unstructured":"Rui Chen, Mengfei Yang, and Xiangying Guo. 2016. Interrupt data race detection based on shared variable access order pattern. Ruan Jian Xue Bao\/Journal of Software 3 (2016), 547\u2013561.","journal-title":"Ruan Jian Xue Bao\/Journal of Software"},{"key":"e_1_3_2_1_6_1","volume-title":"Detecting Out-of-Bounds Array Access Errors in Aerospace Embedded Software. In 2020 7th International Conference on Dependable Systems and Their Applications (DSA). 213\u2013218","author":"Chen Rui","year":"2020","unstructured":"Rui Chen, Tingting Yu, Yunsong Jiang, Chunpeng Jia, Chao Li, Dongdong Gao, and Mengfei Yang. 2020. Detecting Out-of-Bounds Array Access Errors in Aerospace Embedded Software. In 2020 7th International Conference on Dependable Systems and Their Applications (DSA). 213\u2013218. 10.1109\/DSA51864.2020.00038"},{"key":"e_1_3_2_1_7_1","volume-title":"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). 465\u2013471","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 2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C). 465\u2013471. 10.1109\/QRS-C51114.2020.00084"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/1379022.1375618","article-title":"Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs","volume":"43","author":"Flanagan Cormac","year":"2008","unstructured":"Cormac Flanagan, Stephen N Freund, and Jaeheon Yi. 2008. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. ACM SIGPLAN Notices 43, 6 (2008), 293\u2013303.","journal-title":"ACM SIGPLAN Notices"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA","author":"Li Chao","year":"2023","unstructured":"Chao Li, Rui Chen, Boxiang Wang, Zhixuan Wang, Tingting Yu, Yunsong Jiang, Bin Gu, and Mengfei Yang. 2023. An Empirical Study on Concurrency Bugs in Interrupt-Driven Embedded Software. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2023). 1345\u20131356. 10.1145\/3597926.3598140"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. 506\u2013518","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. 10.1145\/3533767.3534412"},{"key":"e_1_3_2_1_11_1","volume-title":"2013 35th International Conference on Software Engineering (ICSE). IEEE, 1444\u20131446","author":"Park Sangmin","year":"2013","unstructured":"Sangmin Park. 2013. Fault comprehension for concurrent programs. In 2013 35th International Conference on Software Engineering (ICSE). IEEE, 1444\u20131446. 10.1109\/icse.2013.6606739"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 2013 International Symposium on Software Testing and Analysis. 134\u2013144","author":"Park Sangmin","year":"2013","unstructured":"Sangmin Park, Mary Jean Harrold, and Richard Vuduc. 2013. Griffin: grouping suspicious memory-access patterns to improve understanding of concurrency bugs. In Proceedings of the 2013 International Symposium on Software Testing and Analysis. 134\u2013144. 10.1145\/2483760.2483792"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1523"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering-Volume 1. 245\u2013254","author":"Park Sangmin","year":"2010","unstructured":"Sangmin Park, Richard W Vuduc, and Mary Jean Harrold. 2010. Falcon: fault localization in concurrent programs. In Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering-Volume 1. 245\u2013254. 10.1145\/1806799.1806838"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-013-0277-y"},{"key":"e_1_3_2_1_16_1","volume-title":"Programming Languages and Systems: 18th European Symposium on Programming, ESOP","author":"Sadowski Caitlin","year":"2009","unstructured":"Caitlin Sadowski, Stephen N Freund, and Cormac Flanagan. 2009. SingleTrack: A dynamic determinism checker for multithreaded programs. In Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22\u201329, 2009. Proceedings 18. Springer, 394\u2013409."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA","author":"Wang Boxiang","year":"2022","unstructured":"Boxiang Wang, Rui Chen, Chao Li, Tingting Yu, Dongdong Gao, and Mengfei Yang. 2022. SpecChecker-ISA: a data sharing analyzer for interrupt-driven embedded software. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2022). 801\u2013804. 10.1145\/3533767.3543295"},{"key":"e_1_3_2_1_18_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 328\u2013342","author":"Wang Chao","year":"2010","unstructured":"Chao Wang, Rhishikesh Limaye, Malay Ganai, and Aarti Gupta. 2010. Trace-based symbolic analysis for atomicity violations. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 328\u2013342."},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 137\u2013146","author":"Wang Liqiang","year":"2006","unstructured":"Liqiang Wang and Scott D Stoller. 2006. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming. 137\u2013146."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 7th Asia-Pacific Symposium on Internet-ware. 199\u2013202","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 Internet-ware. 199\u2013202."}],"event":{"name":"FSE Companion '25: 33rd ACM International Conference on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Clarion Hotel Trondheim Trondheim Norway","acronym":"FSE Companion '25"},"container-title":["Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696630.3728592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,28]],"date-time":"2025-07-28T19:20:19Z","timestamp":1753730419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696630.3728592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":20,"alternative-id":["10.1145\/3696630.3728592","10.1145\/3696630"],"URL":"https:\/\/doi.org\/10.1145\/3696630.3728592","relation":{},"subject":[],"published":{"date-parts":[[2025,6,23]]},"assertion":[{"value":"2025-07-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}