A formal framework for the java bytecode language and verifier

摘要

This paper presents a sound type system for a large subset of the Java bytecode language including classes,interfces,ocnstructors ,methods,exceptions,and byte-code subroutines.This work serves as the foundation for developign a formal specification of the bytecode language and the Java Virtual Machine's bytecode verifier.We also describe a prototype implementation fo a tyep checker for our system and discuss some of the other applciatiosn of this work.for example,we show how to extend our work to examine other program properties,such as the ocrrect use of object locks.