Verification of Java Bytecode using Analysis and Transformation of Logic Programs

Abstract : State of the art analyzers in the Logic Programming (LP) paradigm are nowadays mature and sophisticated. They allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. The aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (JVML). In order to achieve our goal, we rely on well-known techniques for meta-programming and program specialization. More precisely, we propose to partially evaluate a JVML interpreter implemented in LP together with (an LP representation of) a JVML program and then analyze the residual program. Interestingly, at least for the examples we have studied, our approach produces very simple LP representations of the original JVML programs. This can be seen as a decompilation from JVML to high-level LP source. By reasoning about such residual programs, we can automatically prove in the CiaoPP system some non-trivial properties of JVML programs such as termination, run-time error freeness and infer bounds on its resource consumption. We are not aware of any other system which is able to verify such advanced properties of Java bytecode.
Type de document :
Communication dans un congrès
The International Symposium on Practical Aspects of Declarative Languages, 2007, Nice, France. Springer-Verlag, 4354, pp.124-139, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-69611-7_8〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00503986
Contributeur : Laurent Hubert <>
Soumis le : lundi 19 juillet 2010 - 18:08:35
Dernière modification le : jeudi 9 juillet 2015 - 14:42:53
Document(s) archivé(s) le : vendredi 22 octobre 2010 - 16:13:04

Fichiers

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

Identifiants

Collections

Citation

Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, German Puebla. Verification of Java Bytecode using Analysis and Transformation of Logic Programs. The International Symposium on Practical Aspects of Declarative Languages, 2007, Nice, France. Springer-Verlag, 4354, pp.124-139, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-69611-7_8〉. 〈inria-00503986〉

Partager

Métriques

Consultations de la notice

80

Téléchargements de fichiers

489