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.
Type de document :
Communication dans un congrès
9th International Workshop on Verification and Evaluation of Computer and Communication Systems, Sep 2015, Bucarest, Romania. 〈http://vecos.ensta-paristech.fr/2015/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01250600
Contributeur : Jean-Louis Lanet <>
Soumis le : mercredi 6 janvier 2016 - 11:27:30
Dernière modification le : mercredi 16 mai 2018 - 11:24:11
Document(s) archivé(s) le : jeudi 7 avril 2016 - 15:48:05

Fichier

15-Vecos.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01250600, version 1

Citation

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. 〈http://vecos.ensta-paristech.fr/2015/〉. 〈hal-01250600〉

Partager

Métriques

Consultations de la notice

304

Téléchargements de fichiers

100