Subroutines are a major complication for Java bytecode verification:
they are difficult to fit into the data flow analysis that the JVM
specification suggests. We examine the problems that occur with
subroutines and give an overview of the most prominent solutions in
the literature. Using the theorem prover Isabelle/HOL, we have
extended our substantial formalization of the JVM and the bytecode
verifier with its proof of correctness by the most general solution
for bytecode subroutines.
A formalization of the Java bytecode verifier, including
a defensive JVM, exceptions, constructor calls, object initialization, jsr/ret instructions, and arrays:
@inproceedings{KleinW-TPHOLS03,
author = {Gerwin Klein and Martin Wildmoser},
title = {Verified Bytecode Subroutines},
booktitle = {Proceedings of Theorem Proving in Higher Order Logics},
pages = {55--70},
year = {2003},
editor = {David Basin and Burkhard Wolff},
volume = {2758},
series = {Lecture Notes in Computer Science},
url = {\url{http://www4.in.tum.de/~kleing/papers/KleinW-TPHOLS03.html}}
}