Verified Bytecode Verification and Type-Certifying Compilation

Gerwin Klein, Martin Strecker



 
 Abstract

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}
}


Last modified: Thu Jul 30 10:54:42 CEST 2009