Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
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
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
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