@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(davis2014microcode,
 author       = {Jared Davis and Anna Slobodova and Sol Swords},
 year         = {2014},
 title        = {Microcode Verification--Another Piece of the Microprocessor Verification Puzzle},
 booktitle    = {International Conference on Interactive Theorem Proving},
 organization = {Springer},
 pages        = {1--16},
 doi          = {10.1007/978-3-319-08970-6\_1},
)
@inproceedings(hardinucode,
 author       = {David S Hardin and Eric W Smith and William D Young},
 year         = {2006},
 title        = {A robust machine code proof framework for highly secure applications},
 booktitle    = {Proceedings of the Sixth International Workshop on the {ACL2} Theorem Prover and its Applications},
 pages        = {11--20},
 doi          = {10.1145/1217975.1217978},
)
@inproceedings(kaufmann2002efficient,
 author       = {Matt Kaufmann and Rob Sumners},
 year         = {2002},
 title        = {Efficient rewriting of operations on finite structures in ACL2},
 booktitle    = {Proceedings of the 3rd International Workshop on the {ACL2} Theorem Prover and its Applications},
 pages        = {141--150},
)
@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},
)
@inproceedings(fixyourtypes,
 author       = {Sol Swords and Jared Davis},
 year         = {2015},
 title        = {Fix Your Types},
 editor       = {Matt Kaufmann and David L. Rager},
 booktitle    = {{\rm Proceedings Thirteenth International Workshop on the} ACL2 Theorem Prover and Its Applications, {\rm Austin, Texas, USA, 1-2 October 2015}},
 pages        = {3--16},
 doi          = {10.4204/EPTCS.192.2},
)