• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• X86isa

Contributors

Authorship details and acknowledgments.

Original Authors

Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann

Questions or Suggestions? Email Shilpi: shigoel@gmail.com.

Contributors to the x86 ISA Model

Thanks to Rob Sumners for adding support for detecting decode-time exceptions.

Thanks to Alessandro Coglio (Kestrel Institute and Kestrel Technology LLC) for adding support for 32-bit mode and for improving the documentation of these books.

Thanks to Cuong Kim Chau for implementing the floating point instructions and for performing many experiments (along with Keshav Kini) to figure out an efficient configuration for the concrete memory model.

Thanks to Soumava Ghosh for his work on supporting the execution of system calls and the ELF loader functions.

Thanks to Keshav Kini for answering all sorts of git-related questions and for performing many experiments (along with Cuong Kim Chau) to figure out an efficient configuration for the concrete memory model.

Thanks to Robert Krug for carrying out countless arithmetic proofs, and for the initial specification of the paging mechanism and proofs about properties of paging data structures.

Thanks to Ben Selfridge for putting in type declarations and resolving the resulting guard proof obligations about the paging specification functions.

Acknowledgments

This material is based upon work supported by DARPA under Contract No. N66001-10-2-4087.

This material is based upon work supported by the National Science Foundation under Grant Number CNS-1525472.

Thanks to folks formerly at Centaur Technology (including Anna Slobodova, Jared Davis, and Sol Swords) for their suggestions and their wonderful libraries, especially the bitops books.

Thanks to Marijn Heule for contributing his SAT solver for model validation.

Thanks to J Moore for too many things to count.

Thanks to Nathan Wetzler for helpful discussions, especially on proving properties of paging data structures.

Thanks to Arjen van Lith for designing the x86isa logo.