Bit-Blasting ACL2 Theorems
Logic in Computer Science
2011-10-24 v1
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.
Cite
@article{arxiv.1110.4676,
title = {Bit-Blasting ACL2 Theorems},
author = {Sol Swords and Jared Davis},
journal= {arXiv preprint arXiv:1110.4676},
year = {2011}
}
Comments
In Proceedings ACL2 2011, arXiv:1110.4473