REMS: Rigorous Engineering for Mainstream Systems

Researcher positions at Cambridge in Rigorous Engineering for Mainstream Systems (REMS)

How can we use rigorous semantics to improve the quality of mainstream computer systems? REMS (Rigorous Engineering for Mainstream Systems) (link) is a 6-year EPSRC-funded Programme Grant to do just that, bringing together an exciting combination of researchers in systems (architecture, operating systems, and networks) and in semantics (programming languages, automated reasoning, and verification) at three UK universities: Cambridge, Imperial, and Edinburgh.

We want to understand how to build accurate full-scale mathematical models of some of the key computational abstractions (processor architectures, programming languages, and concurrent OS interfaces), and how these can be used for new verification research, to build tools that are applicable to real systems, and to enable new systems and programming language research. Supporting all this, we are also working on new specification tools and their foundations.

If you have a keen interest in developing and applying rigorous methods for real-world systems, we'd like to hear from you. At the Cambridge site, we're looking to appoint several researcher and research-engineer staff: up to four postdocs and two research engineers (we will also be looking to appoint researchers at the Imperial site, advertised separately). We're looking for people who have a strong background in systems, in semantics, or in both, and who want to develop research that integrates theory and practice, contributing to ongoing research and initiating new subprojects. You should have expertise in one or more of the following, on the semantics side:

and/or the following, on the systems side:

We have four postdoctoral researcher positions available. For these positions you should have a PhD (which should be submitted by the start date) or equivalent experience. For candidates with exceptional experience it may be possible to appoint on the Senior Research Associate scale (£37,382-£47,314); for this you should also have the ability to assist with project coordination. These positions are for three years.

We also have two research engineer positions available, which will be on the Research Assistant scale. Candidates for these should have an excellent first degree. One of the positions has a tenure of three years; in some cases it may be possible to combine this with PhD study. The limit of tenure for the other position is one year; this may suit someone who is thinking of going on to a PhD later.

The positions are funded by the EPSRC grant EP/K008528 (link), led by Peter Sewell (link). Further details of the project are at link. Enquiries can be addressed to any of the investigators, listed there.

Those involved in the project include researchers in semantics and systems at Cambridge: Mike Gordon, Magnus Myreen, Andrew Pitts, and Peter Sewell (PI) for the former, and Jon Crowcroft, Steve Hand, Anil Madhavapeddy, Simon Moore, and Robert Watson for the latter, together with Philippa Gardner at Imperial College London and Ian Stark at the University of Edinburgh. Also involved are Mike Dodds (York), Susmit Sarkar (St. Andrews) and Scott Owens (Kent). Project partners include ARM, IBM, Microsoft Research, the FreeBSD foundation, INRIA, U. Pennsylvania, Purdue University, and U. Texas Austin.

Applications should include:

Start date: as soon as possible. The project runs until end February 2019.

For the postdoctoral researcher positions, please quote reference: NR27842. Closing date: 15 May 2013; salary: £27,854-£36,298 pa.

For the research engineer positions, please quote reference NR27832. Closing date: 14 May 2013; salary: £24,049-£27,047 pa. Please indicate the length tenure for which you are applying (one or three years).

Applications should be sent to (preferably as pdf attachments).