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 Group.

Publications

• 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 non-determinism correct.
• 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.

Talks

• Introduction to my work to date (20 July 1995). In DVI, or postscript. (To the Automated Reasoning group.)
• Leaving loops gracefully (30 November 1995). In DVI, or postscript. (To the Automated Reasoning group.)
• A brief summary of the abstract semantics (24 February 1997). In DVI or postscript. (To the "Semantics Lunch" meeting.)
• A talk to the First Intel Symposium on Software Verification (3 November 1998). As they are in colour, the slides are only available in Postscript.

Developments

• 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 retflag component to handle return statements, but, taking a leaf from the definition of SML, uses different "return values".
• The model now does side effects properly.

Problems

• 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

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:

• Paul Curzon
• Konrad Slind
• Mark Staples
• Don Syme
• Myra VanInwegen