## Standard Fixpoint Iteration for Java Bytecode Verification

Java bytecode verification forms the basis for Java-based Internet
security and needs a rigorous description. One important aspect of
bytecode verification is to check if a Java Virtual Machine (JVM)
program is statically well-typed. So far several formal
specifications have been proposed to define what the static
well-typedness means. This paper takes a step further and presents a
chaotic fixpoint iteration, which represents a family of fixpoint
computation strategies to compute a least type for each JVM program
within a finite number of iteration steps. Since a transfer function
in the iteration is not monotone, we choose to follow the example of a
non-standard fixpoint theorem, which requires that all transfer
functions are increasing, and monotone in case the bigger element is
already a fixpoint. The resulting least type is the artificial top
element if and only if the JVM program is not statically well-typed.
The iteration is standard and close to Sun's informal specification
and most commercial bytecode verifiers.

(This paper supersedes two old papers at this place with the titles
"Constraint-Based Specification and Dataflow Analysis for Java(TM) Bytecode Verification" and
"Least Types for Memory Locations in (Java) Bytecode".)

The paper is available as
dvi file and ps file.

Zhenyu Qian