Verified Bytecode Verification and Type-Certifying Compilation

Gerwin Klein and Martin Strecker


This article presents a type certifying compiler for a subset of Java and proves the type correctness of the bytecode it generates in the proof assistant Isabelle. The proof is performed by defining a type compiler that emits a type certificate and by showing a correspondence between bytecode and the certificate which entails well-typing. The basis for this work is an extensive formalization of the Java bytecode type system, which is first presented in an abstract, lattice-theoretic setting and then instantiated to Java types.

Online Copy

Available as [PDF]

Isabelle Sources

Available as [tar.gz]

Bibtex entry

  author =  {Gerwin Klein and Martin Strecker},
  title =   {Verified {B}ytecode {V}erification and Type-Certifying {C}ompilation},
  journal = {Journal of Logic and Algebraic Programming},
  volume =  58,
  number =  {1--2},
  pages =   {27--60},
  year =    2004,
  url =     {\url{}}
Gerwin Klein
2005-01-30 14:03:19