A Provably Correct Stackless Intermediate Representation for Java Bytecode

Delphine Demange 1 Thomas Jensen 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The Java virtual machine executes stack-based bytecode. The intensive use of an operand stack has been identified as a major obstacle for static analysis and it is now common for static analysis tools to manipulate a stackless intermediate representation (IR) of bytecode programs. This paper provides such a bytecode transformation, describes its semantic correctness and evaluates its performance. We provide the semantic foundations for proving that an initial program and its IR behave similarly, in particular with respect to object creation and throwing of exceptions. The correctness of this transformation is proved with respect to a relation on execution traces taking into account that the object allocation order is not preserved by the transformation.
Type de document :
Communication dans un congrès
The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China. Springer-Verlag, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00537815
Contributeur : David Pichardie <>
Soumis le : vendredi 19 novembre 2010 - 14:12:04
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 16:01:44

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00537815, version 1

Citation

Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for Java Bytecode. The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China. Springer-Verlag, 2010, Lecture Notes in Computer Science. 〈inria-00537815〉

Partager

Métriques

Consultations de la notice

350

Téléchargements de fichiers

134