{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:54:33Z","timestamp":1775145273269,"version":"3.50.1"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"ISSTA","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,22]]},"abstract":"<jats:p>Abstract interpretation is widely used to determine programs' numerical properties. However, current abstract domains primarily focus on mathematical semantics, which do not fully capture the complexities of real-world programs relying on machine integer semantics and involving extensive bit-vector operations. This paper presents a solution that combines a bit-level abstraction and a word-level abstraction to capture machine integer semantics. First, we generalize the bit-level abstraction used in the Linux eBPF verifier for determining known and unknown bits of real-world programs, by supplementing all required operations as a standard abstract domain. Based on this abstraction, we design an abstract domain that is signedness-aware and simultaneously retains both the above bit-level and the word-level bound information. These two levels of information cooperate via a standard reduced product operation to improve analysis precision. We implement the proposed domains in the Crab analyzer and the out-of-kernel eBPF verifier PREVAL. Experiments demonstrate their effectiveness in analyzing SV-COMP benchmark programs, assisting hardware designs, and eBPF verification.<\/jats:p>","DOI":"10.1145\/3728905","type":"journal-article","created":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T10:52:56Z","timestamp":1750589576000},"page":"663-685","source":"Crossref","is-referenced-by-count":2,"title":["Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3534-3495","authenticated-orcid":false,"given":"Guangsheng","family":"Fan","sequence":"first","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8084-8009","authenticated-orcid":false,"given":"Liqian","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2449-3287","authenticated-orcid":false,"given":"Banghu","family":"Yin","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2204-4782","authenticated-orcid":false,"given":"Wenyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2025,6,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_12"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882105"},{"key":"e_1_2_1_6_1","volume-title":"Principles of abstract interpretation","author":"Cousot Patrick","year":"2044","unstructured":"Patrick Cousot. 2021. Principles of abstract interpretation. MIT Press. isbn:9780262044905"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800022.808314"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_10_1","unstructured":"CWE-190. 2024. CWE-190: Integer Overflow or Wraparound. https:\/\/cwe.mitre.org\/data\/definitions\/190.html"},{"key":"e_1_2_1_11_1","unstructured":"CWE-191. 2024. CWE-191: Integer Underflow (Wrap or Wraparound). https:\/\/cwe.mitre.org\/data\/definitions\/191.html"},{"key":"e_1_2_1_12_1","unstructured":"CWE-192. 2024. CWE-192: Integer Coercion Error. https:\/\/cwe.mitre.org\/data\/definitions\/192.html"},{"key":"e_1_2_1_13_1","unstructured":"CWE-194. 2024. CWE-194: Unexpected Sign Extension. https:\/\/cwe.mitre.org\/data\/definitions\/194.html"},{"key":"e_1_2_1_14_1","unstructured":"CWE-195. 2024. CWE-195: Signed to Unsigned Conversion Error. https:\/\/cwe.mitre.org\/data\/definitions\/195.html"},{"key":"e_1_2_1_15_1","unstructured":"CWE-196. 2024. CWE-196: Unsigned to Signed Conversion Error. https:\/\/cwe.mitre.org\/data\/definitions\/196.html"},{"key":"e_1_2_1_16_1","unstructured":"CWE-197. 2024. CWE-197: Numeric Truncation Error. https:\/\/cwe.mitre.org\/data\/definitions\/197.html"},{"key":"e_1_2_1_17_1","unstructured":"CWE-680. 2024. CWE-680: Integer Overflow to Buffer Overflow. https:\/\/cwe.mitre.org\/data\/definitions\/197.html"},{"key":"e_1_2_1_18_1","unstructured":"CWE-681. 2024. CWE-681: Incorrect Conversion between Numeric Types. https:\/\/cwe.mitre.org\/data\/definitions\/681.html"},{"key":"e_1_2_1_19_1","unstructured":"Poorna Gaddehosur Dave Thaler. 2021. Making eBPF work on Windows. https:\/\/opensource.microsoft.com\/blog\/2021\/05\/10\/making-ebpf-work-on-windows\/"},{"key":"e_1_2_1_20_1","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911","author":"E\u00e9n Niklas","unstructured":"Niklas E\u00e9n, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA. FMCAD Inc., 125\u2013134. http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651360"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_7"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314590"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480912"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_18"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-95561-8_8"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643778"},{"key":"e_1_2_1_30_1","unstructured":"Juan Jos\u00e9 L\u00f3pez Jaimez and Meador Inge. 2023. Buzzer. https:\/\/github.com\/google\/buzzer"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_1_33_1","unstructured":"Deepak Kapur. 2006. Automatically generating loop invariants using quantifier elimination."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_2"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623186"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575707"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44978-7_10"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_41_1","volume-title":"International Workshop on invariant Generation. 16","author":"Min\u00e9 Antoine","year":"2012","unstructured":"Antoine Min\u00e9. 2012. Abstract domains for bit-level machine integer and floating-point operations. In WING\u201912-4th International Workshop on invariant Generation. 16."},{"key":"e_1_2_1_42_1","volume-title":"Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends\u00ae in Programming Languages, 4, 3-4","author":"Min\u00e9 Antoine","year":"2017","unstructured":"Antoine Min\u00e9. 2017. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends\u00ae in Programming Languages, 4, 3-4 (2017), 120\u2013372."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_38"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275504"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_9"},{"key":"e_1_2_1_48_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and verification in the field: Applying formal methods to $BPF$ just-in-time compilers in the linux kernel. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). 41\u201361."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159974.1134657"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_2_1_51_1","unstructured":"Simon Scannell. 2020. eBPF Fuzzer. https:\/\/scannell.io\/posts\/ebpf-fuzzing"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_22"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3604919"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_27"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_8"},{"key":"e_1_2_1_56_1","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Sun Hao","year":"2024","unstructured":"Hao Sun and Zhendong Su. 2024. Validating the $eBPF$ verifier via state embedding. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). 615\u2013628."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3627703.3629562"},{"key":"e_1_2_1_58_1","unstructured":"Joseph Tafese Isabel Garcia-Contreras and Arie Gurfinkel. 2023. BTOR2MLIR: A Format and Toolchain for Hardware Verification.. In FMCAD. 55\u201363."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"e_1_2_1_62_1","unstructured":"Dmitry Vyukov and Andrey Konovalov. 2015. Syzkaller: an unsupervised coverage-guided kernel fuzzer . https:\/\/github.com\/google\/syzkaller"},{"key":"e_1_2_1_63_1","volume-title":"The k-induction principle","author":"Wahl Thomas","unstructured":"Thomas Wahl. 2013. The k-induction principle. Northeastern University, College of Computer and Information Science, 1\u20132."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454068"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397378"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485495"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591288"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3728905","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T16:56:41Z","timestamp":1752685001000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3728905"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,22]]},"references-count":67,"journal-issue":{"issue":"ISSTA","published-print":{"date-parts":[[2025,6,22]]}},"alternative-id":["10.1145\/3728905"],"URL":"https:\/\/doi.org\/10.1145\/3728905","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,22]]}}}