@misc(acl2:doc,
 author       = {{ACL2 Community}},
 year         = {accessed January, 2017},
 title        = {{ACL2+Books} Documentation},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html},
)
@inproceedings(centaur-framework,
 author       = {{Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt, Jr.}},
 year         = {2011},
 title        = {{A Flexible Formal Verification Framework for Industrial Scale Validation}},
 booktitle    = {{9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2011}},
 pages        = {89--97},
 doi          = {10.1109/MEMCOD.2011.5970515},
)
@incollection(meta,
 author       = {R. S. Boyer and J S. Moore},
 year         = {1981},
 title        = {Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures},
 booktitle    = {The Correctness Problem in Computer Science},
 publisher    = {Academic Press, London},
)
@inproceedings(greve06,
 author       = {David Greve},
 year         = {2006},
 title        = {Parameterized Congruences in ACL2},
 booktitle    = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications},
 series       = {ACL2 '06},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {28--34},
 doi          = {10.1145/1217975.1217981},
)
@inproceedings(meta-05,
 author       = {W. A. Hunt, Jr. and M. Kaufmann and R. B. Krug and J S. Moore and E. W. Smith},
 year         = {2005},
 title        = {Meta Reasoning in {ACL2}},
 editor       = {J. Hurd and T. Melham},
 booktitle    = {18th International Conference on Theorem Proving in Higher Order Logics: {TPHOLs} 2005},
 series       = {Lecture Notes in Computer Science},
 volume       = {3603},
 publisher    = {Springer},
 pages        = {163--178},
 doi          = {10.1007/11541868\_11},
)
@misc(acl2:home,
 author       = {{Matt Kaufmann and J S. Moore}},
 year         = {Accessed: 2016},
 title        = {{ACL2} home page},
 note         = {(see URL \url{http://www.cs.utexas.edu/users/moore/acl2})},
)
@article(trusted-cl-proc,
 author       = {{Matt Kaufmann, J S. Moore, 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},
)
@phdthesis(gl-diss,
 author       = {{Sol Swords}},
 year         = {2010},
 title        = {{A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover}},
 school       = {{Department of Computer Sciences, The University of Texas at Austin}},
 url          = {http://hdl.handle.net/2152/ETD-UT-2010-12-2210},
)
@inproceedings(bit-blasting-GL,
 author       = {{Sol Swords and Jared Davis}},
 year         = {2011},
 title        = {{Bit-Blasting {ACL2} Theorems}},
 booktitle    = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4, 2011.},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)