Part II and MPhil Project Suggestions, 2010-2011

(these will be updated from time to time)

The projects below are outline suggestions - feel free to come and discuss how they could be turned into full proposals, or to suggest others in the general area of applied semantics, especially the relaxed-memory concurrency that real-world multiprocessors exhibit, in verified compilation, or in programming language semantics. Possible supervisors for these include:

What is C, again?

C is part of the foundation of most computer systems, and much effort has been devoted to its standardisation over the years, e.g. with ANSI C from 1989 and C99. Currently a new revision is underway, informally known as C1X, and the WG14 group group has produced a working draft (N1494). But all these are prose documents, without any mathematical semantics, so the basic question, of whether a language implementation meets the standard, is not even precisely defined, let alone testable or provable.

The goal of this project is to give an operational semantics for a modest fragment of C, aiming to capture the intent of the standard. The semantics should be usable as a test oracle: given a small source program, it should be possible to calculate the set of all permitted executions. The choice of the fragment to be covered would be an important early choice: dealing with all of C is almost certainly impractical, so one would expect to cover only a small fragment, but we would probably hope to include at least some of the concurrency aspects. It might be appropriate to express the semantics directly in a functional programming language (e.g. OCaml) or perhaps in a proof assistant or using the Ott tool.

Background:

This is a challenging project which would suit someone with an interest in semantics as it can be applied to real systems. It could well lead in to a PhD in a related area.

Peter.Sewell@cl.cam.ac.uk