[please circulate this to any likely candidates - thanks, Peter]

Research Associate/Senior Research Associate in Applied Semantics for Production Architectures

University of Cambridge Computer Laboratory
Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 - 49,772
Fixed-term: until February 28, 2019, when the grant funding the post currently ends.
Details: http://www.jobs.cam.ac.uk/job/12397/


Do you want to help build mathematically rigorous foundations for real-world computing, to make it more robust and secure?

We have an ongoing project to establish rigorous semantic models for production multiprocessors, to provide a clear basis for programming, software verification, and hardware verification. This involves long-term close collaborations with ARM and IBM, and we have an agreement with ARM to take their internal ISA description, build a mathematical model based on it, integrate it with the concurrency semantics we are developing, and release the whole in a form usable for verification. This will provide the first strongly validated public model for a production multiprocessor architecture. We also have a close collaboration with the CHERI research project, developing processors with hardware-accelerated in-process memory protection and sandboxing, together with an open-source operating system and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the heart of the CHERI design process. For more details, see some of our previous papers:
POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (http://rems.io).

We have a position available to work on:

- the development of our Sail metalanguage for ISA description: a language with a lightweight dependent type system, designed to capture ARM, IBM POWER, and CHERI instruction semantics in an engineer-friendly way;
- translation from Sail to generate efficient emulators and usable theorem-prover definitions;
- mechanised proof about the architecture definitions, e.g. of security properties, relationships between concurrency models, and correctness results for high-level language concurrency compilation; and/or
- development of reasoning, symbolic execution, debugging, and/or model-checking tools above the architecture definitions - the initial work should generate many opportunities along these lines.

The successful candidate must have a PhD (or equivalent experience), a track-record of publication in relevant areas of Computer Science, good knowledge of English and communication skills, and the expertise and commitment to apply rigorous semantics to real systems. We're looking for people with the skills to make solid models and tools, well-engineered and widely usable. You should have expertise in one or more of:

- functional programming (e.g. OCaml)
- programming language semantics and type systems
- theorem provers, especially Isabelle and/or Coq
- symbolic execution
- model-checking

For senior applicants, e.g. who will be able to contribute substantially to future grant applications, it may be possible to appoint at the Senior Research Associate level.

This is part of the broader REMS (Rigorous Engineering for Mainstream Systems) programme grant: a lively collaboration between systems and semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and apply mathematically rigorous semantics to mainstream systems.

Informal enquiries should be directed to Peter Sewell (Peter.Sewell@cl.cam.ac.uk).

To apply online for this vacancy, please click on the 'Apply' button below. This will route you to the University's Web Recruitment System, where you will need to register an account (if you have not already) and log in before completing the online application form.

Please ensure you upload your Curriculum Vitae (CV) and a cover letter explaining your potential contribution to the project, as pdf documents. Include the names of 2 or 3 referees at the appropriate point in the online application. Your referees should be prepared to send references within a week of the closing date, if asked by the University. If you upload any additional documents which have not been requested, we will not be able to consider these as part of your application.

Please quote reference NR10978 on your application and in any correspondence about this vacancy.

The University values diversity and is committed to equality of opportunity.

The University has a responsibility to ensure that all employees are eligible to live and work in the UK.