Verified Lightweight Bytecode Verification

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 and ps.gz
 

BibTeX Entry

@article{KleinN-CPE01,
        author = "Gerwin Klein and Tobias Nipkow",
        title = "Verified Lightweight Bytecode Verification",
        journal = "Concurrency and Computation: Practice and Experience",
        year = "2001",
        volume = "13",
        number = "13",
        editor = "Gary T. Leavens and Susan Eisenbach",
        pages = "1133-1151",
        url = {http://www4.informatik.tu-muenchen.de/~kleing/papers/cpe01.html},
        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 in the theorem prover
Isabelle/HOL and proved soundness and completeness.},
        note = {Invited contribution to special issue on Formal Techniques for Java},
}