Certified Decision Procedures for Width-Independent Bitvector Predicates

Watch a 16-minute conference presentation from OOPSLA 2025 that introduces novel mechanized decision procedures for width-independent bitvector predicates in the Lean interactive theorem prover. Learn how researchers from the University of Cambridge address the gap in automation for width-independent bitvector reasoning by developing certified algorithms that view classical decision procedures through the lens of model checking, where formulas correspond to automata and correctness becomes a safety property. Discover the mechanization of key model checking algorithms including k-induction, automata reachability, automata emptiness checking, and automata minimization, which enable scalable decision procedures for bitvector predicates. Explore the implementation of MBA-Blast, a fast algorithm for controlled fragments mixing arithmetic and bitwise operations commonly found in deobfuscation literature, which outperforms general procedures on specific fragments. Examine evaluation results on benchmarks from compiler problems including Hacker's Delight and LLVM peephole optimizer, as well as equivalence checking for program obfuscation, where the tools achieve 100% success on Hacker's Delight, 100% on deobfuscation datasets with two tools, and up to 27% on LLVM peephole rewrites. Understand how these decision procedures provide push-button automation for width-independent bitvector reasoning in interactive theorem provers and establish foundational algorithms for fast, formally verified model checking.