Bit-Blasting ACL2 Theorems
The work
| Authors | Sol Swords; Jared Davis |
|---|---|
| Editors | |
| Type | article |
| Year | 2011 |
| Citekey | swords2011bitblasting |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Publisher | Open Publishing Association |
| Volume | 70 |
| Pages | 84--102 |
Identifiers
| arXiv | 1110.4676 from its oa_pdf_url |
|---|---|
| DOI | 10.4204/eptcs.70.7 |
| OpenAlex | W2077391533 |
Access
| Landing page | https://doi.org/10.4204/eptcs.70.7 |
|---|---|
| Free full text | https://arxiv.org/pdf/1110.4676 |
Related
| Distinct from | davis2013verified |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
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.
A copy is held
pdf, 193.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-22 14:22 UTC |
| Approved by | a person 2026-09-23 14:05 UTC |
Filed under
Cite it as
@article{swords2011bitblasting,
title = {Bit-Blasting ACL2 Theorems},
author = {Sol Swords and Jared Davis},
year = {2011},
journal = {Electronic Proceedings in Theoretical Computer Science},
publisher = {Open Publishing Association},
volume = {70},
pages = {84--102},
doi = {10.4204/eptcs.70.7},
}
This record lives at https://refs.drheap.org/swords2011bitblasting/ and will keep doing so.