Hanbing Liu, 9/18/02

This Wednesday I will talk about our JVM model M3, M5 and maybe something
about the "M6", if I have time.

I will present what features of a JVM is modeled with those models, and
how those features are modeled. I will also talk about the current
research that goes around the JVM models.

As for researches going around the models, we have two broad categories.
Properties of the JVM itself, and the properties of the concrete programs
that run on the JVMs.

In this first category, I studied the correctness of two versions of the
bytecode verification algorithms using M3. J and George did some work
relating programs executions on M3 and M4 (m3 with threads) in order to
promote a correctness statement on M3 to a one on M4. We need to study
those reduction techniques to make proving concrete program correctness
easiler.

In the second category, Jeff has been building a set of tools for proving
concrete programs on M5(M3, M4) easier.  J has done a proof about the
behavior of a mutlithread program (the apprentice challenge)