HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

An Approach for Formal Verification of Updated Java Bytecode Programs

Abstract : This paper deals with formal specification and verification of Java bytecode update. Programs update for java applications has gained a wide interest since it is used for several purposes: transforming semantics of a program, adding features to a program or performing optimizations. In this paper, we focus on program transformations for java programs 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. Our approach for formal specification and verification of updated Java bytecode programs is based on four ingredients: a formal interpretation of the semantics of update operations, a functional representation of bytecode, bytecode annotation and predicate transformation calculus. We use the concept of Hoare predicate transformation to derive a specification of an annotated bytecode. Annotations are used to express update operations within the code. A functional representation is used to model annotations and bytecode. The approach derives then a new specification for the annotated bytecode using a weakest precondition calculus defined to deal with update operations. Verification conditions are then generated and proved to establish the correction of the update.
Complete list of metadata

Contributor : Jean-Louis Lanet Connect in order to contact the contributor
Submitted on : Wednesday, January 6, 2016 - 11:27:30 AM
Last modification on : Friday, February 4, 2022 - 3:22:37 AM
Long-term archiving on: : Thursday, April 7, 2016 - 3:48:05 PM


Files produced by the author(s)


  • HAL Id : hal-01250600, version 1


Razika Lounas, Mohamed Mezghiche, Jean-Louis Lanet. An Approach for Formal Verification of Updated Java Bytecode Programs. 9th International Workshop on Verification and Evaluation of Computer and Communication Systems, Sep 2015, Bucarest, Romania. ⟨hal-01250600⟩



Record views


Files downloads