Sciweavers

Share
CARDIS
2006
Springer

A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods

12 years 1 months ago
A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods
Ahead-of-Time and Just-in-Time compilation are common ways to improve runtime performances of restrained systems like Java Card by turning critical Java methods into native code. However, native code is much bigger than Java bytecode, which severely limits or even forbids these practices for devices with memory constraints. In this paper, we describe and evaluate a method for reducing nativelycompiled code by suppressing runtime exception check sites, which are emitted when compiling bytecodes that may potentially throw runtime exceptions. This is made possible by completing the Java program with JML annotations, and using a theorem prover in order to formally prove that the compiled methods never throw runtime exceptions. Runtime exception check sites can then safely be removed from the generated native code, as it is proved they will never be entered. We have experimented our approach on several card-range and embedded Java applications, and were able to remove almost all the excepti...
Alexandre Courbot, Mariela Pavlova, Gilles Grimaud
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CARDIS
Authors Alexandre Courbot, Mariela Pavlova, Gilles Grimaud, Jean-Jacques Vandewalle
Comments (0)
books