Asserting Bytecode Safety
We instantiate an Isabelle/HOL framework for proof carrying code to
Jinja bytecode, a downsized variant of Java bytecode featuring objects,
inheritance, method calls and exceptions. Bytecode annotated in a first
order expression language can be certified not to produce arithmetic
overflows. For this purpose we use a generic verification
condition generator, which we have proven correct and relatively
complete.
pdf
BibTeX:
@inproceedings{WildmoserN-ESOP05,
author = {Martin Wildmoser and Tobias Nipkow},
title = {Asserting Bytecode Safety},
booktitle ={Proceedings of the 14th European Symposium on Programming (ESOP 2005)},
editor = {Mooly Sagiv},
series = LNCS,
publisher = "Springer Verlag",
volume = "3444",
pages = "326--341",
year = 2005
}