|
|
|---|
|
|
|
|---|
W. A. Hunt, Jr. and M. Kaufmann, “Towards
a Formal Model of the x86 ISA”, University of Texas at Austin,
Computer Science Department Technical Report TR-12-07, May, 2012.
Relevance:
a “toy model” of the x86, built as a warm up exercise
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.
This work preceded the development of the full x86 model described in bib::ghk13, bib::ghkg14, bib::goel16, and bib::ghk17.