Towards a Formal Model of the X86 ISA
University of Texas at Austin Austin United States
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.
- Computer Programming and Software