@PhdThesis{Klein-PhD,
  author =       {Gerwin Klein},
  title =        {Verified Java Bytecode Verification},
  school =       {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
  year =         {2003},
  url =          {\url{http://www4.in.tum.de/~kleing/diss/}},
  abstract =     {The bytecode verifier is an important part of Java's security
architecture. This thesis presents a fully formal, executable, and
machine checked specification of a representative subset of the Java
Virtual Machine and its bytecode verifier together with a proof that
the bytecode verifier is safe.

The specification consists of an abstract framework for bytecode
verification which is instantiated step by step with increasingly
expressive type systems covering all of the interesting and complex
properties of Java bytecode verification: classes, objects,
inheritance, virtual methods, exception handling, constructors, object
initialization, bytecode subroutines, and arrays.

The instantiation yields two executable verified bytecode verifiers:
the iterative data flow algorithm of the standard Java
platform and also a lightweight bytecode verifier for resource-constrained 
devices such as smart cards.

All specifications and proofs have been carried out in the interactive
theorem prover Isabelle/HOL. Large parts of the proofs are written in
the human-readable proof language Isabelle/Isar making it possible to
understand and reproduce the reasoning independently of the theorem
prover. All formal proofs in this thesis are machine checked and
generated directly from Isabelle sources.},
}