• 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
          • Dynamic-instrumentation
        • Utils
        • Debugging-code-proofs
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • X86isa

Model-validation

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

Doc. topic coming soon! For now, here's an illustrative image.

Subtopics

Dynamic-instrumentation
Utilities to instrument a program run on the model