Treffer: Verified Bytecode Subroutines.

Subroutines are a major complication for Java bytecode verification: they are difficult to fit into the data flow analysis that the Java Virtual Machine (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. [ABSTRACT FROM AUTHOR]