Certified Decision Procedures for Width-Independent Bitvector Predicates
summary
Mechanized, executable decision procedures in Lean for width-independent bitvectors that formalize k-induction, automata reachability, emptiness checking and minimization and expose two tactics: BV_automata (automata-based, complete for a large fragment) and BV_MBA (specialized, very fast on mixed boolean–arithmetic). Evaluation solves 100% of Hacker’s Delight, two tools solve 100% of a deobfuscation MBA dataset, and up to 27% of LLVM peephole rewrites; artifacts and reproducible builds are available.
AI-written summary · about
chapters (10)
- 0:00Width-independent bitvector solvers
- 1:06Alive verifies compiler transformations
- 3:36Parametric bitvector solver goal
- 4:38Decision procedure via automata
- 7:07Automata for bitwise ops
- 8:53Reduction to automata equality
- 9:56Lean proof backends
- 11:00Mixed boolean arithmetic algorithm
- 12:24Benchmark performance
- 13:27Future work and conclusion
related talks
19mPanel: Compilation Frameworks
18mThe Complex(ity) Landscape of Checking Infinite Descent
30mBit-Precise Reasoning via Int-Blasting
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
18mRegular Expression Matching using Bit Vector Automata
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
13mProgram Analysis via Efficient Symbolic Abstraction
23mLet Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…)