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.
ps
BibTeX:
@inproceedings{Nipkow-FOSSACS01,author={Tobias Nipkow},
title={Verified Bytecode Verifiers},
booktitle=
{Foundations of Software Science and Computation Structures (FOSSACS 2001)},
editor={F. Honsell, M. Miculan},publisher=Springer,series=LNCS,volume=2030,
pages={347--363},year=2001}
The theory as presented in the paper has been superseded by a more
streamlined development which has become part of the Java subset
Jinja.