@misc(intel-manuals,
 title        = {{Intel 64 and IA-32 Architectures Software Developer's Manuals.}},
 howpublished = {{Online}},
 note         = {{Order Number: 325462-059US. (June 2016). \newline\url {http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html}.}},
)
@article(pintool,
 author       = {{Chi-Keung Luk, Robert Cohn, Robert Muth, Harish Patil, Artur Klauser, Geoff Lowney, Steven Wallace, Vijay Janapa Reddi, and Kim Hazelwood}},
 year         = {2005},
 title        = {{Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation}},
 journal      = {SIGPLAN Not.},
 volume       = {40},
 number       = {6},
 pages        = {190--200},
 doi          = {10.1145/1064978.1065034},
)
@inproceedings(qemu,
 author       = {{Fabrice Bellard}},
 year         = {2005},
 title        = {{QEMU, a Fast and Portable Dynamic Translator}},
 booktitle    = {Proceedings of the {FREENIX} Track: 2005 {USENIX} Annual Technical Conference, April 10-15, 2005, Anaheim, CA, {USA}},
 pages        = {41--46},
 url          = {http://www.usenix.org/events/usenix05/tech/freenix/bellard.html},
)
@misc(mach-o,
 title        = {{OS X ABI Mach-O File Format Reference}},
 howpublished = {{Online; accessed: January 2017}},
 note         = {{\newline\url {https://developer.apple.com/library/mac/documentation/DeveloperTools/Conceptual/MachORuntime/index.html}}},
)
@inproceedings(records,
 author       = {{Matt Kaufmann and Rob Sumners}},
 title        = {{Efficient Rewriting of Operations on Finite Structures in ACL2}},
 booktitle    = {{Proceedings of $3$rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002)}},
)
@article(systemvabi,
 author       = {{Michael Matz, Jan Hubicka, Andreas Jaeger, and Mark Mitchell}},
 year         = {2005},
 title        = {{Chapter 4: Object Files in System V Application Binary Interface}},
 journal      = {AMD64 Architecture Processor Supplement, Draft v0},
 volume       = {99},
)
@inproceedings(stobjs,
 author       = {{Robert S. Boyer and J S. Moore}},
 year         = {2002},
 title        = {{Single-Threaded Objects in ACL2}},
 booktitle    = {{Practical Aspects of Declarative Languages, 4th International Symposium, {PADL} 2002, Portland, OR, USA, January 19-20, 2002, Proceedings}},
 pages        = {9--27},
 doi          = {10.1007/3-540-45587-6\_3},
)
@inproceedings(raymoore,
 author       = {{Sandip Ray and J S. Moore}},
 year         = {2004},
 title        = {{Proof Styles in Operational Semantics}},
 booktitle    = {{Formal Methods in Computer-Aided Design, 5th International Conference, {FMCAD} 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings}},
 pages        = {67--81},
 doi          = {10.1007/978-3-540-30494-4\_6},
)
@article(ray-mechanical,
 author       = {{Sandip Ray, Warren A. Hunt Jr., John Matthews, and J S. Moore}},
 year         = {2008},
 title        = {{A Mechanical Analysis of Program Verification Strategies}},
 journal      = {J. Autom. Reasoning},
 volume       = {40},
 number       = {4},
 pages        = {245--269},
 doi          = {10.1007/s10817-008-9098-1},
)
@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}},
)
@inproceedings(goel-vstte-13,
 author       = {{Shilpi Goel and Warren A. Hunt, Jr.}},
 year         = {2014},
 title        = {{Automated Code Proofs on a Formal Model of the x86}},
 booktitle    = {{Verified Software: Theories, Tools, Experiments (VSTTE'13)}},
 series       = {{Lecture Notes in Computer Science}},
 volume       = {8164},
 publisher    = {{Springer Berlin Heidelberg}},
 pages        = {222--241.},
 doi          = {10.1007/978-3-642-54108-7\_12},
)
@inproceedings(abstract-stobjs,
 author       = {{Shilpi Goel, Warren A. Hunt Jr. and Matt Kaufmann}},
 year         = {2013},
 title        = {{Abstract Stobjs and Their Application to ISA Modeling}},
 booktitle    = {{Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2013, Laramie, Wyoming, USA, May 30-31, 2013.}},
 pages        = {54--69},
 doi          = {10.4204/EPTCS.114.5},
)
@inbook(x86isa-procos,
 author       = {{Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann}},
 year         = {2017},
 title        = {{Engineering a Formal, Executable x86 ISA Simulator for Software Verification}},
 pages        = {173--209},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-48628-4\_8},
)
@inproceedings(Goel:Syscalls,
 author       = {{Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh}},
 year         = {2014},
 title        = {{Simulation and Formal Verification of x86 Machine-code Programs that Make System Calls}},
 booktitle    = {{Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014}},
 pages        = {91--98},
 doi          = {10.1109/FMCAD.2014.6987600},
)
@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}},
 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 of the 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(hunt-kaufmann-fmcad-2012,
 author       = {{Warren A. Hunt Jr. and Matt Kaufmann}},
 year         = {2012},
 title        = {{A Formal Model of a Large Memory that Supports Efficient Execution}},
 booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge, UK, October 22-25, 2012},
 pages        = {60--67},
 url          = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462556},
)