Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 13-minute conference presentation from OOPSLA 2025 that introduces bv_decide, the first end-to-end verified bitblaster designed for interactive bitvector reasoning in dependently-typed interactive theorem provers. Learn how this groundbreaking tool addresses the longstanding challenges of effective bitvector reasoning within interactive theorem provers, which has hindered their adoption for mechanized proofs despite the clear demand for efficient bitvector reasoning infrastructure in compiler backend verification, cryptographic algorithms, and hardware design. Discover how the research team overcame limitations including incomplete bitvector libraries, unavailable decision procedures, complex operations, and limited host language integration by developing a scalable, completely verified bitblaster with end-to-end proof that trusts only the Lean compiler and kernel. Understand the innovative use of Lean's Functional But In-Place (FBIP) paradigm to efficiently encode core data structures like AIGs, demonstrating that fast SMT solver execution need not compromise rigorous formalization. Examine the comprehensive bitvector library design that supports all SMT-LIB 2.7 standard operations with reasoning principles, including overflow modeling, and offers fast execution with comprehensive API and automation for bit-width-independent reasoning. Review the thorough evaluation results showing bv_decide solving more theorems than the state-of-the-art verified bit-blasting tool CoqQFBV on the full SMT-LIB dataset, plus the verification of over 7000 SMT statements extracted from LLVM representing the largest mechanized verification of LLVM rewrites to date. Gain insights into how this work enables effective, dependable white-box reasoning for bitvector-level verification by making bit-blasting bitvector reasoning a polished, well-supported, and interactive feature of modern interactive theorem provers.
