Verified lightweight bytecode verification
Gerwin Klein, Tobias Nipkow · Concurrency and Computation Practice and Experience · 2001
Abstract Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one‐pass verification of well‐typedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness. Copyright © 2001 John Wiley & Sons, Ltd.