PhD CASE Studentship on ARM architectural semantics

Applications are invited for a fully funded EPSRC CASE PhD studentship at the University of Cambridge Computer Laboratory, with industrial sponsorship from ARM Ltd. The academic supervisor will be Prof. Peter Sewell, and the studentship will build on work by Sarkar, Sewell, and others on mathematically rigorous specifications of the ARM multiprocessor architecture, as described at http://www.cl.cam.ac.uk/~pes20/weakmemory.

You should have a strong background in Computer Science, ideally in both logic and semantics and in computer architecture, and a keen desire to apply rigorous techniques to the problems of real multiprocessors. Possible PhD topics include, for example:

development of a random test methodology for processors being designed, linking a rigorous architectural model to an RTL simulation environment;
verification of multiprocessor interconnects with respect to an architectural model; and
development of daemonic software emulators from architectural models.

The industrial contact is Richard Grisenthwaite, ARM Lead Architect; the studentship would involve regular meetings with ARM staff and perhaps summer internship employment at ARM Cambridge.

For a home student or `eligible' EU student (who has spent at least 3 years working or studying in the UK), the award would provide maintenance, tuition fees, and an industrial top-up (we would expect to apply to another source to fund college fees, of ~2.5k p.a.). For an exceptional non-eligible EU student, the same may be possible, otherwise the maintenance component would not be funded. Unfortunately the award does not fund non-EU international student fees.

Possible start dates are 10 April 2013 or 1 October 2013; it might also be possible to backdate to 1 January 2013.

Informal enquiries, including a CV and a brief description of your interests and relevant background, should be made by email to Peter Sewell.