Verified Bytecode Verifiers

Tobias Nipkow

This paper presents another important step towards a complete formal machine-checked design of the Java Virtual Machine. Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verifier in the style of Kildall's algorithm for a significant subset of the JVM. First an abstract framework for proving correctness of data flow based type inference algorithms for typed assembly languages is formalized. It is shown that under certain conditions Kildall's algorithm yield a correct bytecode verifier. Then the framework is instantiated with a model of the JVM.




@inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
title={Verified Bytecode Verifiers},
{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
editor={F. Honsell, M. Miculan},publisher=Springer,series=LNCS,volume=2030,
The theory as presented in the paper has been superseded by a more streamlined development which has become part of the Java subset Jinja.