@misc(acl2-manual,
 title        = {{ACL2} Theorem Prover and Community Books: User Manual},
 howpublished = {Online; accessed: September 2018},
 note         = {\newline\url {http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual}},
)
@misc(acl2:books:codewalker,
 title        = {{ACL2 Books: Codewalker}},
 howpublished = {{Online; accessed: September 2018}},
 note         = {\newline\url {https://github.com/acl2/acl2/tree/master/books/projects/codewalker}},
)
@misc(acl2:books:rtl-rel11,
 title        = {{ACL2 Books: {\tt rtl/rel11} - A Formal Theory of Register-Transfer Logic and Computer Arithmetic}},
 howpublished = {{Online; accessed: September 2018}},
 note         = {\newline\url {https://github.com/acl2/acl2/tree/master/books/rtl/rel11}},
)
@misc(acl2:books:y86,
 title        = {{ACL2 Books: y86 Specifications}},
 howpublished = {{Online; accessed: September 2018}},
 note         = {\newline\url {https://github.com/acl2/acl2/tree/master/books/models/y86}},
)
@misc(apt-www,
 title        = {{APT} ({Automated Program Transformations}): Web page},
 howpublished = {Online; accessed: September 2018},
 note         = {\newline\url {http://www.kestrel.edu/home/projects/apt}},
)
@mastersthesis(baumann2008formal,
 author       = {Christoph Baumann},
 year         = {2008},
 title        = {Formal Specification of the x86 Floating-Point Instruction Set},
 school       = {Universit{\"a}t des Saarlandes},
 note         = {Online; accessed: September 2018. \newline\url {http://www-wjp.cs.uni-saarland.de/publikationen/Ba08.pdf}},
)
@article(coglio-pop,
 author       = {Alessandro Coglio},
 year         = {2014},
 title        = {Pop-Refinement},
 journal      = {Archive of Formal Proofs},
 note         = {Formal proof development. \newline\url {http://afp.sf.net/entries/Pop_Refinement.shtml}},
)
@inproceedings(apt-simplify,
 author       = {Alessandro Coglio and Matt Kaufmann and Eric Smith},
 year         = {2017},
 title        = {A Versatile, Sound Tool for Simplifying Definitions},
 booktitle    = {Proc.\ 14th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2017})},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.249.5},
)
@phdthesis(degenbaev2012formal,
 author       = {Ulan Degenbaev},
 year         = {2012},
 title        = {Formal Specification of the x86 Instruction Set Architecture},
 school       = {Universit{\"a}t des Saarlandes},
 note         = {Online; accessed: September 2018. \newline\url {http://rg-master.cs.uni-sb.de/publikationen/UD11.pdf}},
)
@incollection(armv7,
 author       = {Anthony Fox and Magnus~O. Myreen},
 year         = {2010},
 title        = {{A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture}},
 editor       = {{Matt Kaufmann and Lawrence C. Paulson}},
 booktitle    = {Interactive Theorem Proving},
 series       = {Lecture Notes in Computer Science},
 volume       = {6172},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {243--258},
 doi          = {10.1007/978-3-642-14052-5\_18},
)
@phdthesis(goel-dissertation,
 author       = {Shilpi Goel},
 year         = {2016},
 title        = {{Formal Verification of Application and System Programs Based on a Validated x86 ISA Model}},
 school       = {{Department of Computer Science, The University of Texas at Austin}},
 note         = {Online; accessed: September 2018. \newline\url {http://hdl.handle.net/2152/46437}},
)
@inproceedings(DBLP:journals/corr/Goel17,
 author       = {Shilpi Goel},
 year         = {2017},
 title        = {The x86isa Books: Features, Usage, and Future Plans},
 booktitle    = {Proc.\ 14th International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2-2017})},
 pages        = {1--17},
 doi          = {10.4204/EPTCS.249.1},
)
@inproceedings(abstract-stobjs,
 author       = {Shilpi Goel and {Hunt Jr.}, Warren~A. and Matt Kaufmann},
 year         = {2013},
 title        = {Abstract Stobjs and Their Application to {ISA} Modeling},
 booktitle    = {Proc.\ International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2-2013})},
 pages        = {54--69},
 doi          = {10.4204/EPTCS.114.5},
)
@inproceedings(x86isa-procos,
 author       = {Shilpi Goel and {Hunt, Jr.}, Warren~A. and Matt Kaufmann},
 year         = {2017},
 title        = {{Engineering a Formal, Executable x86 ISA Simulator for Software Verification}},
 booktitle    = {{Provably Correct Systems}},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {173--209},
 doi          = {10.1007/978-3-319-48628-4\_8},
 note         = {{Editors: Mike Hinchey, Jonathan P. Bowen, and Ernst-R{\"u}diger}},
)
@misc(intel-manuals,
 author       = {{Intel Corporation}},
 title        = {{Intel 64 and IA-32 Architectures Software Developer's Manual}},
 howpublished = {Online; accessed: September 2018},
 note         = {{Order Number: 325462-067US. (May, 2018). \newline\texttt {http://www.intel.com/content/www/us/en/processors/architectures-software-developer\-manuals.html}}},
)
@article(malware64bits,
 author       = {John Leyden},
 year         = {2017},
 title        = {64-bit malware threat may be itty-bitty now, but it's only set to grow},
 journal      = {The Register},
 note         = {Online; accessed: September 2018. \newline\url {https://www.theregister.co.uk/2017/05/24/64bit_malware}},
)
@inproceedings(liu2004java,
 author       = {Hanbing Liu and J~S. Moore},
 year         = {2004},
 title        = {{Java} program verification via a {JVM} deep embedding in {ACL2}},
 booktitle    = {International Conference on Theorem Proving in Higher Order Logics},
 organization = {Springer},
 pages        = {184--200},
 doi          = {10.1007/978-3-540-30142-4\_14},
)
@inproceedings(mccarthy-algol,
 author       = {John McCarthy},
 year         = {1964},
 title        = {{A Formal Description of a Subset of Algol}},
 editor       = {{T. B. Steel}},
 booktitle    = {Formal Language Description Languages for Computer Programming, North Holland, 1966},
 pages        = {1--12},
)
@misc(mechanized-op-semantics,
 author       = {J~S. Moore},
 title        = {{Mechanized Operational Semantics}},
 howpublished = {{Online; accessed: September 2018}},
 note         = {{Lectures in the Marktoberdorf Summer School (August 5-16, 2008).\newline\url {http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html}}},
)
@inproceedings(rocksalt,
 author       = {Greg Morrisett and Gang Tan and Joseph Tassarotti and Jean-Baptiste Tristan and Edward Gan},
 year         = {2012},
 title        = {{RockSalt: Better, Faster, Stronger SFI for the x86}},
 booktitle    = {{Proc.\ of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation}},
 series       = {PLDI '12},
 publisher    = {ACM},
 pages        = {395--404},
 doi          = {10.1145/2254064.2254111},
)
@phdthesis(norrish-c,
 author       = {Michael Norrish},
 year         = {1998},
 title        = {{C} formalised in {HOL}},
 school       = {University of Cambridge},
 note         = {Online; accessed: September 2018. \newline\url {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf}},
)
@inproceedings(reidtrustworthy,
 author       = {Alastair Reid},
 year         = {2016},
 title        = {Trustworthy specifications of ARM $\textsuperscript{\textregistered}$ v8-A and v8-M System level architecture},
 booktitle    = {{2016 Formal Methods in Computer-Aided Design (FMCAD)}},
 pages        = {161--168},
 doi          = {10.1109/FMCAD.2016.7886675},
)
@inproceedings(x86popl,
 author       = {Susmit Sarkar and Peter Sewell and Francesco~Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus Myreen and Jade Alglave},
 year         = {2009},
 title        = {{The Semantics of x86-CC Multiprocessor Machine Code}},
 booktitle    = {Proc.\ 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ({POPL})},
 pages        = {379--391},
 doi          = {10.1145/1594834.1480929},
)
@article(sh:pipeline,
 author       = {Jun Sawada and {Hunt, Jr.}, Warren~A.},
 year         = {2002},
 title        = {{Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability}},
 journal      = {Formal Methods in Systems Design},
 volume       = {20},
 number       = {2},
 pages        = {187--222},
 doi          = {10.1023/A:1014122630277},
)
@article(tso10,
 author       = {Peter Sewell and Susmit Sarkar and Scott Owens and Francesco~Zappa Nardelli and Magnus~O. Myreen},
 year         = {2010},
 title        = {{x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors}},
 journal      = {Communications of the ACM},
 volume       = {53},
 number       = {7},
 pages        = {89--97},
 doi          = {10.1145/1785414.1785443},
)
@phdthesis(gl-diss,
 author       = {Sol Swords},
 year         = {2010},
 title        = {{A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover}},
 school       = {{Department of Computer Science, The University of Texas at Austin}},
 note         = {Online; accessed: September 2018. \newline\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    = {Proc.\ 10th International Workshop on the {ACL2} Theorem Prover and its Applications ({ACL2-2011})},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)