Bit-Blasting ACL2 Theorems

Sol Swords
(Centaur Technology)
Jared Davis
(Centaur Technology)

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 David Hardin and Julien Schmaltz: Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2011), Austin, Texas, USA, November 3-4, 2011, Electronic Proceedings in Theoretical Computer Science 70, pp. 84–102.
Published: 20th October 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: