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 <>
Submitted on : Wednesday, January 6, 2016 - 11:27:30 AM
Last modification on : Thursday, January 7, 2021 - 4:20:39 PM
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