@inproceedings(fmcad14,
 author       = {S. Goel and W.A. Hunt and M. Kaufmann},
 year         = {2014},
 title        = {Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls},
 editor       = {K. Claessen and V. Kuncak},
 booktitle    = {\em{FMCAD'14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design}},
 volume       = {http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/final.pdf},
 publisher    = {EPFL, Switzerland},
 pages        = {91--98},
 doi          = {10.1109/FMCAD.2014.6987600},
)
@book(acs,
 editor       = {M. Kaufmann and P. Manolios and J S. Moore},
 year         = {2000},
 title        = {{Computer-Aided Reasoning: {ACL2} Case Studies}},
 publisher    = {Kluwer Academic Press},
 address      = {Boston, MA.},
)
@book(car,
 author       = {M. Kaufmann and P. Manolios and J S. Moore},
 year         = {2000},
 title        = {{Computer-Aided Reasoning: An Approach}},
 publisher    = {Kluwer Academic Press},
 address      = {Boston, MA.},
 doi          = {10.1007/978-1-4615-4449-4},
)
@inproceedings(acl2-home-page,
 author       = {M. Kaufmann and J S. Moore},
 year         = {2014},
 title        = {The {ACL2} Home Page},
 booktitle    = {\url{http://www.cs.utexas.edu/users/moore/acl2/}},
 publisher    = {Dept. of Computer Sciences, University of Texas at Austin},
)
@inproceedings(wf-guarantee,
 author       = {M. Kaufmann and J S. Moore},
 year         = {2015},
 title        = {Well-Formedness Guarantees for {ACL2} Metafunctions and Clause Processors},
 booktitle    = {(submitted for publication)},
)
@inproceedings(Liu-04,
 author       = {H. Liu and J S. Moore},
 year         = {2004},
 title        = {Java Program Verification via a {JVM} Deep Embedding in {ACL2}},
 editor       = {K. Slind and A. Bunker and G. Gopalakrishnan},
 booktitle    = {17th International Conference on Theorem Proving in Higher Order Logics: {TPHOLs} 2004},
 series       = {Lecture Notes in Computer Science},
 volume       = {3223},
 publisher    = {Springer},
 pages        = {184--200},
 doi          = {10.1007/978-3-540-30142-4\_14},
)
@inproceedings(Moore-Martinez09,
 author       = {J S. Moore and M. Martinez},
 year         = {2009},
 title        = {A Mechanically Checked Proof of the Correctness of the Boyer-Moore Fast String Searching Algorithm},
 booktitle    = {Engineering Methods and Tools for Software Safety and Security (Proceedings of the Martoberdorf Summer School, 2008)},
 publisher    = {IOS Press},
 pages        = {267--284},
 doi          = {10.3233/978-1-58603-976-9-267},
)
@phdthesis(Myreen-09,
 author       = {Magnus O. Myreen},
 year         = {2009},
 title        = {Formal verification of machine-code programs},
 school       = {University of Cambridge},
)
@inproceedings(Myreen-12,
 author       = {Magnus O. Myreen and Konrad Slind and Michael J. C. Gordon},
 year         = {2012},
 title        = {Decompilation into Logic — Improved},
 booktitle    = {Formal Methods in Computer-Aided Design (FMCAD), 2012},
 pages        = {78--81},
)
@techreport(Toibazarov,
 author       = {E. Toibazarov},
 year         = {2013},
 title        = {An ACL2 Proof of the Correctness of the Preprocessing for a Variant of the Boyer-Moore Fast String Searching Algorithm},
 type         = {Honors Thesis},
 institution  = {Computer Science Dept., University of Texas at Austin},
 note         = {See \url{http://www.cs.utexas.edu/users/moore/publications/toibazarov-thesis.pdf}},
)