Ewen Denney

I'm now in Edinburgh.


I am interested in mathematical foundations and tool support for formal program development. Currently, I am employed on a project concerned with the verification of Java Card programs.




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 generally, I am interested in formal methods and, in particular, the mathematical underpinnings and tool support for formal program development.


More about my research on refinement.

Some formal methods links


Ma's e ur toil e, sgrìobh thugam 'sa Ghàidhlig!

Écrivez-moi en français s'il vous plaît!

Ewen Denney

Bureau D074
Campus Universitaire de Beaulieu
35042 RENNES Cedex

Tél. 00 33 2 99 84 75 70
Fax 00 33 2 99 84 25 90

Email denney@irisa.fr

Last modified: Fri Jun 18 17:59:40 MET DST 1999