Ewen Denney

I have worked in IRISA (Rennes), Hong Kong Baptist University, and the University of Edinburgh.

I am interested in mathematical foundations and tool support for formal program development. Specific interests include program synthesis, Java Card, numerical algorithms, and the Palm OS.

My previous page in the Lande group at Irisa, in Rennes.


Program Synthesis

Proof Assistants

A first stab at an automatic translator from HOL to Coq.

Current Interests

Java Card

The Java Card language is a dialect of Java, designed for programming smart cards. The core language is a subset of Java. This has been extended with various libraries (APIs in Java terminology) with specific functionality for smart cards. Smart cards are an important challenge for formal methods for two reasons. Firstly, since code is installed on the cards themselves, the cost of correcting errors could be enormous. Secondly, due to the memory and processing constraints, programs are actually quite small and so amenable to formal reasoning.

We are studying formal aspects of Java Card. We have given a bytecode semantics and used this to prove the correctness of a particular optimisation of the virtual machine. We are concentrating now on the formal development of an optimiser. Future work will include extending our formalisation to the runtime environment.

A talk (in French) giving an overview of Java Card.


More about my research on refinement.
Last modified: Tue Nov 20 18:25:14 GMT 2001