{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:20:18Z","timestamp":1760059218184,"version":"build-2065373602"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/100018693","name":"Horizon Europe","doi-asserted-by":"crossref","award":["101070375"],"award-info":[{"award-number":["101070375"]}],"id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n            Bitvectors are foundational for automated reasoning. A few interactive theorem provers (ITP), such as Lean, have strong support for deciding\n            <jats:italic toggle=\"yes\">fixed-width<\/jats:italic>\n            bitvector predicates by means of bitblasting. However, even these ITPs provide little automation for\n            <jats:italic toggle=\"yes\">width-independent<\/jats:italic>\n            bitvector predicates. To fill this gap, we contribute novel, mechanized decision procedures for width-independent bitvector predicates in Lean. Classical algorithms to decide fragments of width-independent bitvector theory can be viewed from the lens of model checking, where the formula corresponds to an automaton and the correctness of the formula is a safety property. However, we cannot currently use this lens in mechanized proofs, as there are no executable, fast, and formally verified model checking algorithms that can be used interactively\n            <jats:italic toggle=\"yes\">from within<\/jats:italic>\n            ITPs. To fill this gap, we mechanize key algorithms in the model checking literature:\n            <jats:italic toggle=\"yes\">k<\/jats:italic>\n            -induction, automata reachability, automata emptiness checking, and automata minimization. Using these mechanized algorithms, we contribute scalable, mechanized, decision procedures for width-independent bitvector predicates. Furthermore, for controlled fragments of mixtures of arithmetic and bitwise operations which occur in the deobfuscation literature, we mechanize a recent fast algorithm (MBA-Blast), which outperforms the more general procedures on this fragment. Finally, we evaluate our decision procedures on benchmarks from classical compiler problems such as Hacker\u2019s Delight and the LLVM peephole optimizer, as well as on equivalence checking problems for program obfuscation. Our tools solve 100% of Hacker\u2019s Delight, two of our tools solve 100% of the deobfuscation dataset, and up to 27% of peephole rewrites extracted from LLVM\u2019s peephole rewriting test suite. Our new decision procedures provide a push-button experience for width-independent bitvector reasoning in interactive theorem provers, and, more broadly, pave the way for foundational algorithms for fast, formally verified model checking.\n          <\/jats:p>","DOI":"10.1145\/3763148","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2736-2758","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certified Decision Procedures for Width-Independent Bitvector Predicates"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-6410-3681","authenticated-orcid":false,"given":"Siddharth","family":"Bhat","sequence":"first","affiliation":[{"name":"University of Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4719-2922","authenticated-orcid":false,"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"University of Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4234-5131","authenticated-orcid":false,"given":"Chris","family":"Hughes","sequence":"additional","affiliation":[{"name":"Independent Researcher, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[{"name":"University of Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_2_1_2_1","unstructured":"Siddharth Bhat Alex Keizer Chris Hughes Andr\u00e9s Goens and Tobias Grosser. 2024. Verifying Peephole Rewriting In SSA Compiler IRs. arXiv preprint arXiv:2407.03685."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Siddharth Bhat and L\u00e9o Stefanesco. 2025. Certified Decision Procedures for Width- Independent Bitvector Predicates in Interactive Theorem Provers. https:\/\/doi.org\/10.5281\/zenodo.16269885 10.5281\/zenodo.16269885","DOI":"10.5281\/zenodo.16269885"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In TACAS. 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691584"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855755"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.002"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2013.30"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_12_1","unstructured":"Martin Brain James H Davenport and Alberto Griggio. 2017. Benchmarking Solvers SAT-style.. In SC^2@ ISSAC."},{"volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"B\u00fcchi J Richakd","key":"e_1_2_1_13_1","unstructured":"J Richakd B\u00fcchi. 1990. Weak second-order arithmetic and finite automata. In The Collected Works of J. Richard B\u00fcchi. Springer, 398\u2013424."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_7"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_1_18_1","volume-title":"Automata Theory: An Algorithmic Approach","author":"Esparza J.","year":"2023","unstructured":"J. Esparza and M. Blondin. 2023. Automata Theory: An Algorithmic Approach. MIT Press. isbn:9780262376938 lccn:2022052127 https:\/\/books.google.de\/books?id=SP2nEAAAQBAJ"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/259794.259827"},{"key":"e_1_2_1_23_1","volume-title":"Mona: Monadic second-order logic in practice. In TACAS. 89\u2013110.","author":"Henriksen Jesper G","year":"1995","unstructured":"Jesper G Henriksen, Jakob Jensen, Michael J\u00f8rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. 1995. Mona: Monadic second-order logic in practice. In TACAS. 89\u2013110."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0399"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE49443.2020.00023"},{"volume-title":"Automata and computability","author":"Kozen Dexter","key":"e_1_2_1_26_1","unstructured":"Dexter Kozen. 1997. Automata and computability. Springer. isbn:978-0-387-94907-9"},{"key":"e_1_2_1_27_1","volume-title":"X-MBA: Towards Heterogeneous Mixed Boolean-Arithmetic Deobfuscation. In MILCOM 2024-2024 IEEE Military Communications Conference (MILCOM). 1082\u20131087","author":"Li Gengwang","year":"2024","unstructured":"Gengwang Li, Min Yu, Dongliang Fang, Gang Li, Xiang Meng, Jiangguo Jiang, and Weiqing Huang. 2024. X-MBA: Towards Heterogeneous Mixed Boolean-Arithmetic Deobfuscation. In MILCOM 2024-2024 IEEE Military Communications Conference (MILCOM). 1082\u20131087."},{"key":"e_1_2_1_28_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Liu Binbin","year":"2021","unstructured":"Binbin Liu, Junfu Shen, Jiang Ming, Qilong Zheng, Jing Li, and Dongpeng Xu. 2021. $MBA-Blast$: Unveiling and Simplifying Mixed $Boolean-Arithmetic$ Obfuscation. In 30th USENIX Security Symposium (USENIX Security 21). 1701\u20131718."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_1_30_1","unstructured":"Nuno P Lopes and John Regehr. 2018. Future Directions for Optimizing Compilers. arXiv preprint arXiv:1809.02161."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_22"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649837"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Aina Niemetz and Mathias Preiner. 2023. Bitwuzla. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 3\u201317. isbn:978-3-031-37703-7","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_9"},{"volume-title":"Automated reasoning about hardware data types using bit-vectors of symbolic lengths","author":"Pichora Mark Christopher","key":"e_1_2_1_37_1","unstructured":"Mark Christopher Pichora. 2003. Automated reasoning about hardware data types using bit-vectors of symbolic lengths. University of Toronto."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_15"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3560831.3564256"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD). 161\u2013168.","DOI":"10.1109\/FMCAD.2016.7886675"},{"volume-title":"Verification of reactive systems: formal methods and algorithms","author":"Schneider Klaus","key":"e_1_2_1_41_1","unstructured":"Klaus Schneider, Jimmy Shabolt, and John G Taylor. 2004. Verification of reactive systems: formal methods and algorithms. Springer."},{"volume-title":"Hardware and Software","author":"Schuele Tobias","key":"e_1_2_1_42_1","unstructured":"Tobias Schuele and Klaus Schneider. 2007. Verification of Data Paths Using Unbounded Integers: Automata Strike Back. In Hardware and Software, Verification and Testing, Eyal Bin, Avi Ziv, and Shmuel Ur (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 65\u201380. isbn:978-3-540-70889-6"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.1003420 10.5281\/zenodo.1003420","DOI":"10.5281\/zenodo.1003420"},{"key":"e_1_2_1_45_1","unstructured":"Henry S Warren. 2013. Hacker\u2019s delight. Pearson Education."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77535-5_5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763148","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:55Z","timestamp":1760031715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763148"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":47,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763148"],"URL":"https:\/\/doi.org\/10.1145\/3763148","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}