My PhD work
This page is something of a meagre resource at the moment, but I hope
to improve it.
My work concentrated on the development of an embedding of a
formal model for C into the HOL theorem prover. I chose to develop my
own model for C using a structural operational semantics. I submitted
my thesis on 7 August 1998, and was successfully examined on 27
November 1998 by Dr. Andy Gordon and Professor Tom Melham. I
finally graduated in May 1999. My supervisor was Professor Mike Gordon, and I was (and still
am) in the Automated Reasoning
- A paper, Deterministic
expressions in C that appeared as part of the ETAPS99
conference, held in March 1999, in Amsterdam. This article is
copyright Springer-Verlag 1999 and won one of two Best Paper
prizes for the conference.
- My PhD thesis,
available in the form of a lab. technical report.
- A technical
report (also in compressed
DVI) giving an abstract presentation of the semantics used
in Cholera. This does get the details of operator and function
- A paper published as part of the
supplementary proceedings of the TPHOLs'96 conference. It
explains the philosophy motivating my work, and presents some of
my results, though in a fairly vague way. It also makes the
(common) mistake of stating that C's non-deterministic binary
operators evaluate either the left argument and then the right,
or the other way round. This is not correct.
Accompanying the article is a poster (also available at A4 size).
- The Cholera model that I have developed as the
basis for my work on C hasn't changed radically for a while, and
I have a description of it
available. (The document is a literate programming file, and
the standard of the prose is not strong; it's there mainly for
my benefit at this stage.)
- At the end of my first year here (August 1995) I wrote a couple
of first year reports describing my PhD work; a progress report describing what I'd done
up until that date, and a proposal for the tool I hoped to
develop as a result of this work.
I have kept the slides from the talks I have given.
(Prefer the postscript in general, as it does the landscape mode
dvips will convert the DVI files
correctly, and they are much smaller than the postscript.)
Things I've done that either came after I wrote the above, or which
aren't clear from them:
- The Cholera model uses binary words at its
fundamental level, to represent memory. The language modelled
now includes type-casts as a result.
- The model state no longer uses a
return statements, but, taking a leaf
from the definition of SML, uses different "return values".
- The model now does side effects properly.
There are still some flaws in the Cholera model:
- Omissions: The model doesn't do goto
statements, switch statements or floating point values.
- Basic flaws: The model assumes that every
integral value has a unique representation in terms of bytes.
This is not true, though it is often true of C implementations.
Formal methods resources
The best place to start is undoubtedly the World-wide
Web Virtual Library: Formal Methods at Oxford.
Some of the people I work with (i.e., these are the people that I
pester when I can't figure out how to do something in HOL) include:
Michael Norrish <Michael.Norrish@cl.cam.ac.uk>
Last modified: Mon Oct 7 15:21:50 BST 2002