Toward a Provably-Correct Implementation of the JVM Bytecode Verifier

This paper reports on our ongoing efforts to realize a provably-correct implementation of the Java Virtual Machine bytecode verifier. We take the perspective that bytecode verification is a data flow analysis problem, or more generally, a constraint-solving problem on lattices. We employ Specware, a system available from Kestrel Institute that supports the development of programs from specifications, to formalize the bytecode verifier, and to formally derive an executable program from our specification.

The paper is available as doc file.

Zhenyu Qian