Accession Number:

AD1024616

Title:

Towards a Formal Model of the X86 ISA

Descriptive Note:

Technical Report

Corporate Author:

University of Texas at Austin Austin United States

Personal Author(s):

Report Date:

2012-03-30

Pagination or Media Count:

198.0

Abstract:

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:

APPROVED FOR PUBLIC RELEASE