A formal framework for the Java bytecode language and verifier

This paper presents a sound type system for a large subset of the Java byte code language including classes, interfaces, constructors, methods, excepti ons, and bytecode subroutines. This work serves as the foundation for devel oping a formal specification of the bytecode language and the Java Virtual Machine's bytecode verifier. We also describe a prototype implementation of a type checker for our system and discuss some of the other applications o f this work. For example, we show how to extend our work to examine other p rogram properties, such as the correct use of object locks.