Ewen Denney


Je suis maintenant à Édimbourg (Écosse).

Anglais

Je suis intéressé par les bases mathématiques et les outils pour le développement formel de programmes. Actuellement, je suis post-doctorant sur un projet concerné par la vérification de programmes Java Card.


 

Recherche

 

Java Card

Le langage Java Card est un dialecte de Java, conçu pour programmer les cartes à puces. Le Java Card est un sous-ensemble de Java, étendu par diverses bibliothèques (APIs dans la terminologie de Java) spécifiques pour les cartes à puces. Les cartes à puces sont un défi important pour des méthodes formelles pour deux raisons. Premièrement, puisque le code est installé sur les cartes elles-mêmes, le coût de correction d'erreurs pourrait être énorme. Deuxièmement, en raison des contraints physiques sur la mémoire et le processeur, programmes sont assez petits, et se pretent bien au raisonnement formel.

Nous sommes en train d'étudier des aspects formels de Java Card. Nous avons donné une sémantique du bytecode que nous a permit de prouver la correction d'une optimisation particulière de la machine virtuelle. Nous nous concentrons maintenant sur le développement formel d'un optimiseur. Les travaux futurs incluront l'extension de notre formalisation à l'environnement d'exécution (JCRE).

Un exposé donnant un survol de Java Card.

Plus généralement, je suis intéressé par les méthodes formelles et, en particulier, les fondements mathématiques pour les outils pour le développement formel de programmes.

Raffinement

Plus de détailes sur mes recherches sur le raffinement de programmes.

Quelques liens sur les méthodes formelles

Info


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
IRISA
Campus Universitaire de Beaulieu
35042 RENNES Cedex
France

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 18:01:02 MET DST 1999