Verified Lightweight Bytecode Verification

(journal version)

Gerwin Klein and Tobias Nipkow


Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one-pass verification of welltypedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness.

Online Copy

Available as [PDF]

Isabelle Sources

See here.

Bibtex entry

  author = {Gerwin Klein and Tobias Nipkow},
  title = {Verified Lightweight Bytecode Verification},
  journal = {Concurrency and Computation: Practice and Experience},
  editor = {S. Eisenbach and G. T. Leavens},
  publisher = {John Wiley and Sons},
  volume = 13,
  number = 13,
  pages = {1133-1151},
  year = 2001
  url = {\url{}}
Gerwin Klein
2005-01-30 14:05:49