Lightweight Bytecode Verification

Abstract
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 for µJava in the theorem prover Isabelle/HOL and mechanically verified soundness and completeness.
Lightweight Bytecode Verification is used in the KVM of Sun's Java 2 Micro Edition. It is called preverification there.
This research is closely associated with Project Bali.
Papers
Gerwin Klein and Tobias Nipkow: Verified Lightweight Bytecode Verification. In: Formal Techniques for Java Programs, Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and Müller, P. and Poetzsch-Heffter, A. (Eds.). Technical Report 269, 5/2000, Fernuniversität Hagen. (extended abstract [pdf] [ps.gz]) [bibtex]
ECOOP 2000 Workshop proceedings available from here.

Gerwin Klein and Tobias Nipkow: Verified Lightweight Bytecode Verification. In: Concurrency: Practice and Experience, Eisenbach, S. and Leavens, G. T. (Eds.). 2001; 13(13) (journal preprint version [pdf] [ps.gz]) [bibtex]
Isabelle theories
The µJava Isabelle theories online.
Isabelle proofs
All µJava Isabelle theories and Isabelle/Isar proofs as pdf document
Just the lightweight bytecode verifier stuff in a separate pdf document.

Last modified: Fri Jun 23 16:03:52 CEST 2000