Proof-Directed De-compilation of Low-Level Code

Abstract. We present a proof theoretical method for de-compiling lowlevel code to the typed lambda calculus. We first define a proof system for a low-level code language based on the idea of Curry-Howard isomorphism. This allows us to regard an executable code as a proof in intuitionistic propositional logic. As being a proof of intuitionistic logic, it can be translated to an equivalent proof of natural deduction proof system. This property yields an algorithm to translate a given code into a lambda term. Moreover, the resulting lambda term is not a trivial encoding of a sequence of primitive instructions, but reflects the behavior of the given program. This process therefore serves as proof-directed decompilation of a low-level code language to a high-level language. We carry out this development for a subset of Java Virtual Machine instructions including most of its features such as jumps, object creation and method invocation. The proof-directed de-compilation algorithm has been...

• Type: Conference
• Year: 2001
• Where: ESOP
• Authors: Shin-ya Katsumata, Atsushi Ohori
• Keywords: Deduction Proof System, ESOP 2001, Low-level Code Language, Programming Languages, Proof Theoretical Method