Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
images
machine
portcullis
proofs
tools/execution
utils
.gitignore
Makefile
README
acl2-customization.lsp
cert.acl2
doc.acl2
doc.lisp
top.acl2
top.lisp

README

----------------------------------------------------------------------
             A Formal and Executable Model of the x86 ISA
          and the associated x86 Machine-Code Analysis Framework

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

----------------------------------------------------------------------

These files contain a specification of the x86 instruction set
architecture (ISA); we characterize x86 machine instructions and model
the instruction fetch, decode, and execute process using the ACL2
theorem-proving system.  They also contain proofs of correctness of
some x86 machine-code programs.

Up-to-date documentation is available at:
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____X86ISA

Questions/Comments? Contact Shilpi Goel (shigoel@cs.utexas.edu).

----------------------------------------------------------------------