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.
This research is closely associated with Project Bali.
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]
Just the lightweight bytecode verifier stuff in a separate pdf document.
|Gerwin Klein||Last modified: Fri Jun 23 16:03:52 CEST 2000|