Towards a Formal Model of the X86 ISA
Warren Jr A Hunt, Matt Kaufmann · 2012
Abstract : We present a preliminary formalization of a subset of the x86 instruction set. Our model is writtenin the logic of the ACL2 theorem prover. It can be executed as a Lisp program on concrete data, whichprovides the capability to validate the model against results delivered by actual x86 processors. Wedemonstrate how bugs in our model can also be eliminated by using the ACL2 prover to verify guards(semantic preconditions) for our functions.