Towards a General Framework for Formal Reasoning about Java Bytecode Transformation

Razika Lounas
(University of Boumerdes, Algeria)
Mohamed Mezghiche
(University of Boumerdes, Algeria)
Jean-Louis Lanet
(Universityof Limoges, France)

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

In Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine: Proceedings Fourth International Symposium on Symbolic Computation in Software Science (SCSS 2012), Gammarth, Tunisia, 15-17 December 2012, Electronic Proceedings in Theoretical Computer Science 122, pp. 63–73.
Published: 30th July 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: