Proof-Directed De-compilation of Low-Level Code

13 years 10 months ago
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...
Shin-ya Katsumata, Atsushi Ohori
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where ESOP
Authors Shin-ya Katsumata, Atsushi Ohori
Comments (0)