Adapted from Hanbing's email to acl2-mtg:

On this Wednesday meeting, I will give a talk based the paper

The first part is a 30 minutes practice talk for my presentation at the IVME03 workshop on June 12th.

The paper is an experience report about building an executable model of the JVM. On the one hand, our JVM model contains enough details for it to be considered as a "conventional" machine emulator. On the other hand, our methodology allows us to reason about the machine emulator analytically.