• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Software-verification
• Hardware-verification
• Projects

X86isa

x86 ISA model and machine-code analysis framework developed at UT Austin

Subtopics

Program-execution

Setting up the x86 ISA model for a program run

Introduction

A Formal and Executable Model of the x86 Instruction Set Architecture

X86isa-build-instructions

Building books related to the x86 ISA and the machine-code analysis framework

Publications

Technical publications related to these x86isa books

Contributors

Authorship Details and Acknowledgments

Machine

Core elements of the x86 ISA, like the x86 state, decoder function, etc., and proofs about the x86 ISA specification.

Implemented-opcodes

Intel Opcodes Supported in x86isa

Proof-utilities

Basic utilities for x86 machine-code proofs

To-do

Known issues, planned activities, wishlists, etc.

Concrete-simulation-examples

Model-validation

How do we trust that our x86 ISA model is faithful to the real machine?

Utils

Utilities for rest of the X86ISA books

Debugging-code-proofs