References

  1. 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..
  2. 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.
  3. 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.
  4. OS X ABI Mach-O File Format Reference. Online; accessed: January 2017. https://developer.apple.com/library/mac/documentation/DeveloperTools/Conceptual/MachORuntime/index.html.
  5. 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).
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org