[TYPES/announce] Research position on relaxed memory model design

[Scott Owens]

We invite applications to a one year research post at the University of Kent in
Canterbury, UK on the EPSRC-funded project "Relaxed Memory Model Design for
Theory and Practice".

The project builds on our previous work in rigorously understanding and
reasoning with existing real-world concurrency models, including those of x86,
PowerPC, and C/C++.  It aims to create a new design that is more
understandable, and has better support for formal reasoning, while still
maintaining acceptable performance.  This is a wide-open area, and the
researcher will have the opportunity to influence the direction of the research
overall.  Possible topics include:
- verification of compiler optimisations
- verification of concurrent algorithms
- analysis of the performance of concurrent algorithms
- semantic theories of shared memory concurrency

The researcher will work closely with the project's PI, Dr Scott Owens, and will
have significant input into the direction of their own research.  They will also
have the opportunity to work with project partners in Prof. Peter Sewell's group
at the University of Cambridge and Dr Francesco Zappa Nardelli's group at INRIA
Paris-Rocquencourt.

The post is suitable for a researcher with experience on topics in any of the
following or related areas:
- concurrent or distributed algorithms
- concurrency theory
- automated reasoning or interactive theorem proving
- software verification, including Hoare logic and separation logic
- programming language design
- semantics

Closing date: 15 November, 2013
Interviews to be held in the first week of December.

To apply for the position, search for Ref STM0414 at the Kent jobs web site
http://jobs.kent.ac.uk/fe/tpl_kent01.asp?newms=se.

Please direct any questions about the post to Scott Owens
(S.A.Owens at kent.ac.uk).