{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T17:23:25Z","timestamp":1783445005464,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":89,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T00:00:00Z","timestamp":1645488000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Natural Science Foundation of China","award":["62002195"],"award-info":[{"award-number":["62002195"]}]},{"name":"Australian Research Grants","award":["DP210101348"],"award-info":[{"award-number":["DP210101348"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,2,28]]},"DOI":"10.1145\/3503222.3507770","type":"proceedings-article","created":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T20:49:01Z","timestamp":1645562941000},"page":"859-872","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Path-sensitive and alias-aware typestate analysis for detecting OS bugs"],"prefix":"10.1145","author":[{"given":"Tuo","family":"Li","sequence":"first","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jia-Ju","family":"Bai","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shi-Min","family":"Hu","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,2,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Program analysis and specialization for the C programming language. Ph. D. Dissertation","author":"Andersen Lars Ole","unstructured":"Lars Ole Andersen. 1994. Program analysis and specialization for the C programming language. Ph. D. Dissertation. University of Cophenhagen."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCCC.2016.7835996"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594299"},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the 2019 USENIX Annual Technical Conference (ATC). 255\u2013268","author":"Bai Jia-Ju","year":"2019","unstructured":"Jia-Ju Bai, Julia Lawall, Qiu-Liang Chen, and Shi-Min Hu. 2019. Effective static analysis of concurrency use-after-free bugs in Linux device drivers. In Proceedings of the 2019 USENIX Annual Technical Conference (ATC). 255\u2013268."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3381990"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 2016 USENIX Annual Technical Conference (ATC). 635\u2013647","author":"Bai Jia-Ju","year":"2016","unstructured":"Jia-Ju Bai, Yu-Ping Wang, Jie Yin, and Shi-Min Hu. 2016. Testing error handling code in device drivers using characteristic fault injection. In Proceedings of the 2016 USENIX Annual Technical Conference (ATC). 635\u2013647."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3088515.3088517"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 2010 International Conference on Formal Methods in Computer-Aided Design (FMCAD). 35\u201342","author":"Ball Thomas","year":"2010","unstructured":"Thomas Ball, Ella Bounimova, Rahul Kumar, and Vladimir Levin. 2010. SLAM2: static driver verification with under 4% false alarms. In Proceedings of the 2010 International Conference on Formal Methods in Computer-Aided Design (FMCAD). 35\u201342."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485547"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.24"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14896-0_5"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 8th International Symposium on Operating Systems Design and Implementation (OSDI). 209\u2013224","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs.. In Proceedings of the 8th International Symposium on Operating Systems Design and Implementation (OSDI). 209\u2013224."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349311"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250789"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950396"},{"key":"e_1_3_2_1_16_1","unstructured":"2021. Clang: an LLVM-based C\/C++ compiler. http:\/\/clang.llvm.org\/"},{"key":"e_1_3_2_1_17_1","unstructured":"2021. CLOC: count lines of code. https:\/\/cloc.sourceforge.net"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771811"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2013.44"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134069"},{"key":"e_1_3_2_1_21_1","unstructured":"2021. Coverity: a commercial static analysis tool. https:\/\/scan.coverity.com\/"},{"key":"e_1_3_2_1_22_1","unstructured":"2021. Coverity reports for Linux kernel. https:\/\/github.com\/torvalds\/linux\/search?q=coverity&type=commits"},{"key":"e_1_3_2_1_23_1","unstructured":"2021. Coverity reports for Zephyr project. https:\/\/github.com\/zephyrproject-rtos\/zephyr\/labels\/Coverity"},{"key":"e_1_3_2_1_24_1","unstructured":"2021. Cppcheck: a tool for static C\/C++ code analysis. http:\/\/cppcheck.sourceforge.net\/"},{"key":"e_1_3_2_1_25_1","unstructured":"2021. Clang Static Analyzer. https:\/\/clang-analyzer.llvm.org\/"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/358438.349309"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/773473.178263"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_27"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA419626"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00025"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348255"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250764"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512539"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480911"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2011.5764696"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378855"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/325478.325519"},{"key":"e_1_3_2_1_39_1","unstructured":"2021. Facebook Infer: a tool to detect bugs in Java and C\/C++\/Objective-C code. https:\/\/fbinfer.com\/"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268973"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2019.00022"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375613"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179519"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359662"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2009.10.004"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390645"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855840.1855852"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250766"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_3"},{"key":"e_1_3_2_1_50_1","unstructured":"2021. LLVM compiler infrastructure. https:\/\/llvm.org\/"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354244"},{"key":"e_1_3_2_1_52_1","volume-title":"Proceedings of the 28th USENIX Security Symposium. 1769\u20131786","author":"Lu Kangjie","year":"2019","unstructured":"Kangjie Lu, Aditya Pakki, and Qiushi Wu. 2019. Detecting missing-check bugs via semantic-and context-aware criticalness and constraints inferences. In Proceedings of the 28th USENIX Security Symposium. 1769\u20131786."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000008666.56394.a1"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1357010.1352618"},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 30th USENIX Security Symposium. 181\u2013198","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: don\u2019t interpret, compile!. In Proceedings of the 30th USENIX Security Symposium. 181\u2013198."},{"key":"e_1_3_2_1_57_1","volume-title":"Proceedings of the 24th USENIX Security Symposium. 49\u201364","author":"Ramos David A","year":"2015","unstructured":"David A Ramos and Dawson Engler. 2015. Under-constrained symbolic execution: correctness checking for real code. In Proceedings of the 24th USENIX Security Symposium. 49\u201364."},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings of the 10th International Symposium on Operating Systems Design and Implementation (OSDI). 279\u2013292","author":"Renzelmann Matthew J","year":"2012","unstructured":"Matthew J Renzelmann, Asim Kadav, and Michael M Swift. 2012. SymDrive: testing drivers without devices. In Proceedings of the 10th International Symposium on Operating Systems Design and Implementation (OSDI). 279\u2013292."},{"key":"e_1_3_2_1_59_1","unstructured":"2021. RIOT: a real-time multi-threading operating system. https:\/\/github.com\/RIOT-OS\/RIOT"},{"key":"e_1_3_2_1_60_1","volume-title":"Proceedings of the 26th USENIX Security Symposium. 167\u2013182","author":"Schumilo Sergej","year":"2017","unstructured":"Sergej Schumilo, Cornelius Aschermann, Robert Gawlik, Sebastian Schinzel, and Thorsten Holz. 2017. kAFL: hardware-assisted feedback fuzzing for OS kernels. In Proceedings of the 26th USENIX Security Symposium. 167\u2013182."},{"key":"e_1_3_2_1_61_1","unstructured":"2021. Project to study faults in Linux.. https:\/\/github.com\/coccinelle\/faults-in-Linux"},{"key":"e_1_3_2_1_62_1","unstructured":"V Shakti D Shekar BB Meshram and MP Varshapriya. 2012. Device driver fault simulation using KEDR. International Journal of Advanced Research in Computer Engineering and Technology 580\u2013584."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380346"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192418"},{"key":"e_1_3_2_1_65_1","unstructured":"2021. Smatch: a static bug-finding tool for C. http:\/\/smatch.sourceforge.net\/"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854043"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3168364"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2302311"},{"key":"e_1_3_2_1_70_1","unstructured":"2021. SVF wiki. https:\/\/github.com\/SVF-tools\/SVF\/wiki\/Detecting-memory-leaks"},{"key":"e_1_3_2_1_71_1","unstructured":"2021. Syzkaller: a kernel fuzzer. https:\/\/github.com\/google\/syzkaller"},{"key":"e_1_3_2_1_72_1","volume-title":"Proceedings of the 30th USENIX Security Symposium.","author":"Seyed Talebi Seyed Mohammadjavad","year":"2021","unstructured":"Seyed Mohammadjavad Seyed Talebi, Zhihao Yao, Ardalan Amiri Sani, Zhiyun Qian, and Daniel Austin. 2021. Undo workarounds for kernel bugs. In Proceedings of the 30th USENIX Security Symposium."},{"key":"e_1_3_2_1_73_1","unstructured":"2021. TencentOS-tiny: a real-time IoT operating system developed by Tencent. https:\/\/github.com\/Tencent\/TencentOS-tiny"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380386"},{"key":"e_1_3_2_1_75_1","volume-title":"Proceedings of the 2021 USENIX Annual Technical Conference (ATC). 31\u201345","author":"Wang Wenwen","year":"2021","unstructured":"Wenwen Wang. 2021. MLEE: effective detection of memory leaks on early-exit paths in OS kernels. In Proceedings of the 2021 USENIX Annual Technical Conference (ATC). 31\u201345."},{"key":"e_1_3_2_1_76_1","unstructured":"2021. WLLVM: whole program LLVM. https:\/\/github.com\/travitch\/whole-program-llvm"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610395"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.06.010"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3134600.3134620"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_20"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772985"},{"key":"e_1_3_2_1_84_1","volume-title":"Proceedings of the 25th USENIX Security Symposium. 363\u2013378","author":"Yun Insu","year":"2016","unstructured":"Insu Yun, Changwoo Min, Xujie Si, Yeongjin Jang, Taesoo Kim, and Mayur Naik. 2016. APISan: sanitizing API usages through semantic cross-checking. In Proceedings of the 25th USENIX Security Symposium. 363\u2013378."},{"key":"e_1_3_2_1_85_1","unstructured":"2021. Z3: a theorem prover. https:\/\/github.com\/Z3Prover\/z3"},{"key":"e_1_3_2_1_86_1","unstructured":"2021. Zephyr: a scalable real-time operating system. https:\/\/github.com\/zephyrproject-rtos\/zephyr"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409686"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660213"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328464"}],"event":{"name":"ASPLOS '22: 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Lausanne Switzerland","acronym":"ASPLOS '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3503222.3507770","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3503222.3507770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:49Z","timestamp":1750188649000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3503222.3507770"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,22]]},"references-count":89,"alternative-id":["10.1145\/3503222.3507770","10.1145\/3503222"],"URL":"https:\/\/doi.org\/10.1145\/3503222.3507770","relation":{},"subject":[],"published":{"date-parts":[[2022,2,22]]},"assertion":[{"value":"2022-02-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}