Towards a General Framework for Formal Reasoning about Java Bytecode Transformation
Logic in Computer Science
2013-08-01 v1 Programming Languages
Abstract
Program transformation has gained a wide interest since it is used for several purposes: altering semantics of a program, adding features to a program or performing optimizations. In this paper we focus on program transformations at the bytecode level. Because these transformations may introduce errors, our goal is to provide a formal way to verify the update and establish its correctness. The formal framework presented includes a definition of a formal semantics of updates which is the base of a static verification and a scheme based on Hoare triples and weakest precondition calculus to reason about behavioral aspects in bytecode transformation
Cite
@article{arxiv.1307.8212,
title = {Towards a General Framework for Formal Reasoning about Java Bytecode Transformation},
author = {Razika Lounas and Mohamed Mezghiche and Jean-Louis Lanet},
journal= {arXiv preprint arXiv:1307.8212},
year = {2013}
}
Comments
In Proceedings SCSS 2012, arXiv:1307.8029