Asserting Bytecode Safety

Martin Wildmoser, Tobias Nipkow

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.



  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