Treffer: Verified Bytecode Subroutines
Title:
Verified Bytecode Subroutines
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publication Year:
2003
Collection:
CiteSeerX
Document Type:
Fachzeitschrift
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.EDDECF0B
Database:
BASE
Weitere Informationen
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.