Verified Bytecode Verification and Type-Certifying Compilation

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 gzip tar, awaiting integration into the Isabelle distribution...
 

BibTeX Entry

@Article{klein04:_formal_compil_bytec_verif,
  author = 	 {Gerwin Klein and Martin Strecker},
  title = 	 {Verified Bytecode Verification and
                   Type-Certifying Compilation},
  journal = 	 {The Journal of Logic and Algebraic Programming},
  year = 	 2004,
  volume =	 58,
  pages =	 {27-60}
}