Ewen Denney
I'm now in Edinburgh.
Français
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.
Research
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.
Refinement
More about my research
on refinement.
-
A Theory of Program Refinement : (ps,
pdf,
abstract)
My thesis was on the theory of refinement calculi, with an eye
on how choices made in the formalism have a bearing on practical issues.
Program refinement is a formal method in which a program is gradually
derived from a specification, using rules of a calculus in which the intermediate
stages of development are recorded. Refinement is not a program development
methodology, as such, but rather a framework for recording and reusing
developments, and so should be seen as part of a larger framework for programming
as a whole. In my thesis, I studied the theoretical issues which arise
in its formalisation, by working with a simple idealised language and program
logic, and formalising the refinement theory this induces together with
its semantics. The refinement calculus is a lambda-calculus extended with
existential variables and first-order logic. We prove that this is conservative
over the underlying logic.
-
Simply-typed Underdeterminism : dvi,
ps
An extension of the simply-typed lambda calculus for formalising the
concept of underdeterminism. This allows us to express stubs and
skeletons which give rise to the notion of partiality in top-down program
and proof development. We axiomatise a simple notion of program refinement
and give a semantics, for which the calculus is proven sound and complete.
-
Refinement Types for Specification : ps
A theory of program specification based on the notion of refinement
type. This provides a notion of structured specification. We axiomatise
the satisfaction of specifications by programs as a generalised typing
relation and give rules for refining specifications. A per semantics based
on Henkin models is given, and the calculus proven sound and complete.
-
Refining Refinement Types : dvi,
ps,
abstract
More details and a slightly different semantics.
Some formal methods links
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 17:59:40 MET DST 1999