Bit-Blasting ACL2 Theorems
arXiv:1110.4676 · doi:10.4204/EPTCS.70.7
Abstract
Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.
In Proceedings ACL2 2011, arXiv:1110.4473
Cited by in corpus (14)
- Extending ACL2 with SMT Solvers
- Fix Your Types
- Modeling Algorithms in SystemC and ACL2
- New Rewriter Features in FGL
- Verified AIG Algorithms in ACL2
- ACL2s Systems Programming
- Term-Level Reasoning in Support of Bit-blasting
- Meta-extract: Using Existing Facts in Meta-reasoning
- The x86isa Books: Features, Usage, and Future Plans
- Adding 32-bit Mode to the ACL2 Model of the x86 ISA
- Incremental SAT Library Integration Using Abstract Stobjs
- Computing and Proving Well-founded Orderings through Finite Abstractions
- RV32I in ACL2
- A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract)