[Prev][Next][Index][Thread]
New paper on Java bytecode subroutines
TITLE:
Simple Verification Technique for Complex Java Bytecode Subroutines
AUTHOR:
Alessandro Coglio
ABSTRACT:
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.
Regards,
Alessandro Coglio
Computer Scientist @ Kestrel Institute