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