A declarative approach to Java Virtual Machine modelisation and Bytecode execution

  • Gérome Laffineur

Thèse de l'étudiant: Master typesMaster en sciences informatiques

Résumé

Algorithm recognition, which is the problem of verifying whether a program
implements a given algorithm, is an important topic in program analysis. This
work is in the continuity of the framework for algorithm recognition in binary
code defined in [25]. This article describes a transformation based approach
to compare algorithms written in Horn clauses. We propose a decompiler that
translate Java bytecode programs (.jar) into a declarative CLP representation
based on Horn clauses. The first purpose of this decompiler is to act as the
front-end of the framework described in [25]. The particularity of the approach
presented here is that we propose a direct translation between bytecode instructions
and the declarative representation (i.e. without an intermediate representation).
Keywords
Decompiler, Java Virtual Machine (JVM), Constraint Logic Programming (CLP),Horn
clauses, Bytecode.
Date de réussite23 juin 2017
langueAnglais
Institution diplomante
  • Université de Namur
SuperviseurAnthony Cleve (Président) & Wim Vanhoof (Promoteur)

Citer ceci

A declarative approach to Java Virtual Machine modelisation and Bytecode execution
Laffineur, G. (Auteur). 23 juin 2017

Thèse de l'étudiant: Master typesMaster en sciences informatiques