• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• X86isa

Publications

Technical publications related to these x86isa books

From the oldest to the newest:

1. Warren A. Hunt, Jr. and Matt Kaufmann. Towards a Formal Model of the x86 ISA. Technical Report, Department of Computer Science, The University of Texas at Austin.
2. Warren A. Hunt, Jr. and Matt Kaufmann. A Formal Model of a Large Memory that Supports Efficient Execution. In Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22-25), 2012
3. Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann. Abstract Stobjs and Their Application to ISA Modeling. In Proceedings of the ACL2 Workshop 2013, EPTCS 114, pp. 54-69, 2013
4. Shilpi Goel and Warren A. Hunt, Jr. Automated Code Proofs on a Formal Model of the x86. In Verified Software: Theories, Tools, Experiments (VSTTE 13), volume 8164 of Lecture Notes in Computer Science, pages 222 241. Springer Berlin Heidelberg, 2014
5. Shilpi Goel, Warren A. Hunt, Jr., Matt Kaufmann, and Soumava Ghosh. Simulation and Formal Verification of x86 Machine-Code Programs That Make System Calls. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD 14), pages 18:91 98, 2014
6. Shilpi Goel. Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. Ph.D. Dissertation, Department of Computer Science, The University of Texas at Austin. 2016
7. Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann. Engineering a Formal, Executable x86 ISA Simulator for Software Verification. In Provably Correct Systems (ProCoS), 2017
8. Shilpi Goel. The x86isa Books: Features, Usage, and Future Plans. In the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2017
9. Alessandro Coglio and Shilpi Goel. Adding 32-bit Mode to the ACL2 Model of the x86 ISA. In the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 Workshop), 2018
10. Shilpi Goel and Rob Sumners. Using x86isa for Microcode Verification. In the Workshop on Instruction Set Architecture Specification (SpISA), 2019.
11. Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords. Verifying x86 Instruction Implementations. In the proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2020.