Reasoning about Y86 Machine Code
J Strother Moore
April 27, 2011

Abstract: In this talk I talk about some
preliminary work aimed at developing techniques to
reason about machine code for Warren Hunt's ACL2
model of Bryant and O'Hallaron's Y86 ISA.  The
techniques include developing a notion of the
``effects'' of a computation, Greve's ``wormhole
abstraction'' to avoid explicit description of
irrelevant state components, separating
``extensional'' from ``intentional'' resources of
the machine, ``snorkeling'' to permit relatively
long symbolic executions (through thousands of
instructions), and generic theorems packaged with
macros to make it more convenient to reason about
straight-line code, loops, and Y86-style procedure
calls.