Veried Bytecode Veriers

Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verier in the style of Kildall’s algorithm for a signicant subset of the Java Virtual Machine. First an abstract framework for proving correctness of data ow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall’s algorithm yields a correct bytecode verier. Then the framework is instantiated with our previous work about the JVM. Finally we demonstrate the exibility of the framework by extending our previous JVM model and the executable bytecode verier with object initialization.