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

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:

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 2014 or 1 October 2014.

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