Accession Number:



Towards a Formal Model of the X86 ISA

Descriptive Note:

[Technical Report, Technical Report]

Corporate Author:

University of Texas at Austin

Personal Author(s):

Report Date:


Pagination or Media Count:



We present a preliminary formalization of a subset of the x86 instruction set. Our model is written in the logic of the ACL2 theorem prover. It can be executed as a Lisp program on concrete data, which provides the capability to validate the model against results delivered by actual x86 processors. We demonstrate how bugs in our model can also be eliminated by using the ACL2 prover to verify guards semantic preconditions for our functions.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

[A, Approved For Public Release]