[TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

[Peter Sewell]

On 15 December 2016 at 23:20, Peter Sewell <Peter.Sewell at cl.cam.ac.uk>
wrote:

> [please circulate this to any likely candidates - thanks, Peter]
>
> Research Associate/Senior Research Associate in Applied Semantics for
> Production Architectures
>

Updating this: the likellihood of new funding means we may be able to make
several appointments, to build a really strong team.   Closing date 24 Jan,
as before.

Peter



> 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 at 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.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20170112/be1b5544/attachment-0001.html>