A PhD studentship on “Reasoning about Racy Programs under Relaxed Consistency” is available in the School of Computer Science at the University of St Andrews, funded by Microsoft Research and EPSRC.

The project will involve developing reasoning principles and tools for relaxed memory consistency settings. This is a key problem in shared-memory concurrency at the low-level, whether in C or C++, or even higher-level languages such as Java.

The project will be supervised by Dr Susmit Sarkar at the University of St Andrews. Dr Jade Alglave of Microsoft Research Cambridge will be the Microsoft supervisor. During the course of their PhD, Scholars are invited to Microsoft Research in Cambridge for an annual Summer School, and there is also a possibility of paid internships during studies. The studentship is fully funded to pay fees and stipend for students with a relevant connection to the UK.

Applicants are expected to have or expect to obtain a UK first-class Honours or Masters degree (or its equivalent from non-UK institutions) in Computer Science, but the minimum standard we require is an upper second-class Honours degree or equivalent. Some experience in concurrent and/or functional programming and an aptitude for mathematical subjects are required. Knowledge and experience of one or more of formal verification, mechanised proofs, and programming languages is highly desirable.

For further information on how to apply, see our postgraduate web pages. Ideally the student will start in October 2015, or as soon as possible thereafter. Further details on the project and suggested reading is available from Dr Susmit Sarkar.