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
summer internship employment at ARM Cambridge.
- development of a random test methodology for processors being
designed, linking a rigorous architectural model to an RTL simulation
- verification of multiprocessor interconnects with respect to
an architectural model; and
- development of daemonic software emulators from architectural
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
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.