Hanbing Liu, 9/25/02

This week, I will continue the talk on modeling the JVM with ACL2 and
related research work on those models M3, M5, and maybe some aspect of
"M6", such as modeling of the machine state, and the related jvm2acl2
tool.

Last time, I am happy many people asked quite a number of questions.
Please remember to bring up questions this time too. I also thank Jeff and
Sandip for commenting here and there. That helps. So please ask us to
clarify whenever necessary.