A declarative approach to Java Virtual Machine modelisation and Bytecode execution

  • Gérome Laffineur

Student thesis: Master types › Master in Computer science

Abstract

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 of Award23 Jun 2017
Original languageEnglish
Awarding Institution
  • University of Namur
SupervisorAnthony Cleve (President) & Wim Vanhoof (Supervisor)

Cite this

Documents

'