The aim of this paper is to prove the correctness of an executable bytecode verifier for the downsized version of Java Virtual Machine (JVM). The authors describe &mgr;, an abstraction of the JVM that works on types rather than values. This new machine is faithful: welltypedness on it guarantees the absence of type errors in the concrete JVM operating &mgr; mode.

The key is the organization of Java data types as a semi-lattice (a partially ordered set with supremum), built on the subclass relation, in which the error type err is the greatest element: let M be a method; its type is the list of the state types characterizing the state of the machine before execution of the corresponding instruction. Then the byte code verifier computes a type t for M such that the absence of err in t means that the M is welltyped.

Such a computation is seen as an iterative data flow analysis on the semi-lattice of types: if the method M has the type t, each stage of the iteration is characterized by the work list w of those elements of t that have changed and whose changes still need to be propagated.

One picks a p in w, removes it from w, executes the corresponding instruction, propagates the new state to the successor instructions of p, and adds the possibly modified elements of t to w. The main result of the paper (theorem 10, p. 605) gives conditions insuring that the previous algorithm yields a correct bytecode verifier.

In the last section, the algorithm is extended to object initialization, in order to test if a new object is properly initialized before it is used.

Because the paper is in the very active domain of Java Virtual Machines, the writing is often condensed and hard to follow by a non-specialist. A good bibliography with very recent references provides useful help.