@misc(acl2:doc,
 author       = {{ACL2 Community}},
 year         = {Accessed: 2020},
 title        = {{ACL2+Books} Documentation},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html},
)
@inproceedings(05-hunt-meta,
 author       = {Hunt Jr., Warren A. and Matt Kaufmann and Robert Bellarmine Krug and J. Strother Moore and Eric Whitman Smith},
 year         = {2005},
 title        = {Meta Reasoning in {ACL2}},
 editor       = {Joe Hurd and Tom Melham},
 booktitle    = {Theorem Proving in Higher Order Logics},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {163--178},
 doi          = {10.1007/11541868_11},
)
@inproceedings(kaufmann-equivalence-2014,
 author       = {Matt Kaufmann and J. Strother Moore},
 year         = {2014},
 title        = {Rough Diamond: An Extension of Equivalence-Based Rewriting},
 editor       = {Gerwin Klein and Ruben Gamboa},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {537--542},
 doi          = {10.1007/978-3-319-08970-6_35},
)
@article(KAUFMANN20093,
 author       = {Matt Kaufmann and J Strother Moore and Sandip Ray and Erik Reeber},
 year         = {2009},
 title        = {Integrating external deduction tools with {ACL2}},
 journal      = {Journal of Applied Logic},
 volume       = {7},
 number       = {1},
 pages        = {3 -- 25},
 doi          = {10.1016/j.jal.2007.07.002},
 note         = {Special Issue: Empirically Successful Computerized Reasoning},
)
@book(russinoff-book-2019,
 author       = {David M. Russinoff},
 year         = {2019},
 title        = {Formal Verification of Floating-Point Hardware Design: A Mathematical Approach},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-95513-1},
)
@inproceedings(17-swords-term-level,
 author       = {Sol Swords},
 year         = {2017},
 title        = {Term-Level Reasoning in Support of Bit-blasting},
 editor       = {Anna Slobodova and Warren A. Hunt, Jr.},
 booktitle    = {{\rm Proceedings 14th International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Austin, Texas, USA, May 22-23, 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {249},
 publisher    = {Open Publishing Association},
 pages        = {95--111},
 doi          = {10.4204/EPTCS.249.7},
)
@misc(fgl-github,
 author       = {Sol Swords},
 year         = {Accessed: 2020},
 title        = {{FGL} source distribution},
 url          = {https://github.com/acl2/acl2/tree/master/books/centaur/fgl},
)
@inproceedings(11-swords-bit-blasting,
 author       = {Sol Swords and Jared Davis},
 year         = {2011},
 title        = {Bit-Blasting {ACL2} Theorems},
 editor       = {David Hardin and Julien Schmaltz},
 booktitle    = {{\rm Proceedings 10th International Workshop} on the ACL2 Theorem Prover and its Applications, {\rm Austin, Texas, USA, November 3-4, 2011}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {70},
 publisher    = {Open Publishing Association},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)