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)
TL;DR
This paper develops a formal framework for verifying the correctness of Java bytecode transformations, ensuring that program updates preserve intended behavior through rigorous semantics and logical reasoning.
Contribution
It introduces a formal semantics for bytecode updates and a verification scheme using Hoare logic and weakest precondition calculus for correctness assurance.
Findings
Framework enables formal verification of bytecode transformations.
Provides a basis for static analysis of program updates.
Ensures behavioral correctness of transformed bytecode.
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
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.