New paper on Java bytecode subroutines

Simple Verification Technique for Complex Java Bytecode Subroutines

Alessandro Coglio

Java is normally compiled to bytecode, which is verified and then executed
by the Java Virtual Machine. Bytecode produced via compilation must pass
verification. The main cause of complexity for bytecode verification is
subroutines, used by compilers to generate more compact code. The
techniques to verify subroutines proposed in the literature reject certain
programs produced by mundane compilers or are otherwise difficult to
realize within an implementation of the Java Virtual Machine. This paper
presents a novel technique which is very simple to understand, implement,
and prove sound. It is also very powerful: the set of accepted programs has
a simple characterization which most likely includes all code generable by
current compilers and which enables future compilers to make more extensive
use of subroutines.

Available at http://www.kestrel.edu/java.


 Alessandro Coglio
 Computer Scientist @ Kestrel Institute