Verified lightweight bytecode verification

Gerwin Klein, Tobias Nipkow

Research output: Contribution to journalArticlepeer-review

23 Scopus citations


An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.

Original languageEnglish
Pages (from-to)1133-1151
Number of pages19
JournalConcurrency and Computation: Practice and Experience
Issue number13
StatePublished - Nov 2001


  • Bytecode verification
  • Data flow analysis
  • Java
  • Theorem proving


Dive into the research topics of 'Verified lightweight bytecode verification'. Together they form a unique fingerprint.

Cite this